Theorem lecon 154

Description: Contrapositive for l.e.

Hypothesis

Ref	Expression
le.1	a ≤ b

Assertion

Ref	Expression
lecon	b⊥ ≤ a⊥

Proof of Theorem lecon

Step	Hyp	Ref	Expression
1		ax-a2 31	. . . 4 (b ∪ a) = (a ∪ b)
2		oran 87	. . . 4 (b ∪ a) = (b⊥ ∩ a⊥ )⊥
3		le.1	. . . . 5 a ≤ b
4	3	df-le2 131	. . . 4 (a ∪ b) = b
5	1, 2, 4	3tr2 64	. . 3 (b⊥ ∩ a⊥ )⊥ = b
6	5	con3 68	. 2 (b⊥ ∩ a⊥ ) = b⊥
7	6	df2le1 135	1 b⊥ ≤ a⊥

Syntax hints:   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This theorem is referenced by:  lecon1 155  lecon3 157  lei3 246  nom14 311  i2or 344  ska4 433  binr1 517  ud4lem1a 577  biao 799  3vded12 815  3vded22 818  3vroa 831  sa5 836  elimconslem 867  comanb 872  marsdenlem3 882  gomaex3h4 905  gomaex3h7 908  gomaex3h11 912  oa3to4lem6 950  oa6todual 952  oa6fromdual 953  oa4to6 965  oa8todual 971  lem3.3.7i4e1 1068  lem3.3.7i5e1 1071

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40  df-le1 130  df-le2 131

Copyright terms: Public domain