Theorem lecon 154

Description: Contrapositive for l.e. (Contributed by NM, 27-Aug-1997.)

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 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

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  1069  lem3.3.7i5e1  1072