Theorem oridm 110

Description: Idempotent law. (Contributed by NM, 10-Aug-1997.)

Assertion

Ref	Expression
oridm	(a ∪ a) = a

Proof of Theorem oridm

Step	Hyp	Ref	Expression
1		ax-a1 30	. . . 4 a = a⊥ ⊥
2		or0 102	. . . . . 6 (a⊥ ∪ 0) = a⊥
3	2	ax-r1 35	. . . . 5 a⊥ = (a⊥ ∪ 0)
4	3	ax-r4 37	. . . 4 a⊥ ⊥ = (a⊥ ∪ 0)⊥
5	1, 4	ax-r2 36	. . 3 a = (a⊥ ∪ 0)⊥
6	5	lor 70	. 2 (a ∪ a) = (a ∪ (a⊥ ∪ 0)⊥ )
7		ax-a5 34	. 2 (a ∪ (a⊥ ∪ 0)⊥ ) = a
8	6, 7	ax-r2 36	1 (a ∪ a) = a

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6  0wf 9

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-t 41  df-f 42

This theorem is referenced by:  anidm  111  orordi  112  orordir  113  omlem1  127  bile  142  lel2or  170  ler2or  172  ledi  174  ledio  176  comid  187  ska15  244  wql1  293  womle2a  295  wbile  401  wledi  405  wledio  406  ka4ot  435  lem3a.1  444  i3bi  496  dfi3b  499  lem4  511  binr3  519  i3abs1  522  i3th5  547  ud1lem3  562  ud4lem2  582  ud5lem3  594  u1lemona  625  u2lemob  631  u3lemob  632  u4lemob  633  u4lem4  759  u5lem4  760  u3lem6  767  u4lem6  768  u5lem6  769  u3lem9  784  biao  799  3vth5  808  3vth6  809  3vth9  812  3vded21  817  3vded22  818  3vroa  831  oau  929  oa23  936  distoa  944  oa3-2lema  978  oa3-2lemb  979  oa3-5lem  984  d3oa  995  oagen1  1014  oadistd  1023  4oagen1  1042  4oadist  1044  ml3le  1129  dp15lema  1154  xdp15  1199  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208