Theorem oridm 102

Description: Idempotent law.

Assertion

Ref	Expression
oridm	(a ∪ a) = a

Proof of Theorem oridm

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

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

This theorem is referenced by:  anidm 103  orordi 104  orordir 105  omlem1 119  bile 134  lel2or 162  ler2or 164  ledi 166  ledio 168  comid 179  ska15 236  wql1 285  womle2a 287  wbile 383  wledi 387  wledio 388  wr5 413  ka4ot 417  lem3a.1 426  i3bi 478  dfi3b 481  lem4 493  binr3 501  i3abs1 504  i3th5 529  ud1lem3 544  ud4lem2 564  ud5lem3 576  u1lemona 607  u2lemob 613  u3lemob 614  u4lemob 615  u4lem4 741  u5lem4 742  u3lem6 749  u4lem6 750  u5lem6 751  u3lem9 766  biao 781  3vth5 790  3vth6 791  3vth9 794  3vded21 799  3vded22 800  3vroa 813  oau 909  oa23 916  distoa 924  oa3-2lema 958  oa3-2lemb 959  oa3-5lem 964  d3oa 975  oagen1 994  oadistd 1003  4oagen1 1021  4oadist 1023

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

This theorem depends on definitions:  df-t 40  df-f 41

metamath.org