Theorem oridm 110

Description: Idempotent law.

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 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 1041  4oadist 1043

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

Copyright terms: Public domain