Theorem lecom 180

Description: Comparable elements commute. Beran 84 2.3(iii) p. 40. (Contributed by NM, 30-Aug-1997.)

Hypothesis

Ref	Expression
lecom.1	a ≤ b

Assertion

Ref	Expression
lecom	a C b

Proof of Theorem lecom

Step	Hyp	Ref	Expression
1		orabs 120	. . . 4 (a ∪ (a ∩ b⊥ )) = a
2	1	ax-r1 35	. . 3 a = (a ∪ (a ∩ b⊥ ))
3		lecom.1	. . . . . 6 a ≤ b
4	3	df2le2 136	. . . . 5 (a ∩ b) = a
5	4	ax-r1 35	. . . 4 a = (a ∩ b)
6	5	ax-r5 38	. . 3 (a ∪ (a ∩ b⊥ )) = ((a ∩ b) ∪ (a ∩ b⊥ ))
7	2, 6	ax-r2 36	. 2 a = ((a ∩ b) ∪ (a ∩ b⊥ ))
8	7	df-c1 132	1 a C b

Syntax hints:   ≤ wle 2   C wc 3  ^⊥ 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-le2 131  df-c1 132

This theorem is referenced by:  comorr  184  coman1  185  gsth  489  gt1  492  i3bi  496  oi3ai3  503  lem4  511  u1lemc6  706  comi12  707  u1lemle1  710  u2lemle1  711  u3lemle1  712  u4lemle1  713  u5lemle1  714  u12lembi  726  u3lem15  795  bi1o1a  798  3vcom  813  3vded21  817  1oa  820  2oalem1  825  mlalem  832  bi3  839  bi4  840  orbi  842  negantlem1  848  elimconslem  867  elimcons  868  comanblem1  870  mhlemlem1  874  mhlem  876  marsdenlem3  882  marsdenlem4  883  mlaconjolem  885  mlaconjo  886  mhcor1  888  e2ast2  894  e2astlem1  895  govar  896  gomaex3lem1  914  gomaex3lem2  915  oa3to4lem1  945  oa3to4lem2  946  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oacom2  1012  oa3moa3  1029  lem4.6.2e1  1082  lem4.6.6i1j3  1094  lem4.6.7  1103