QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud4lem2 GIF version

Theorem ud4lem2 582
Description: Lemma for unified disjunction. (Contributed by NM, 23-Nov-1997.)
Assertion
Ref Expression
ud4lem2 ((a ∪ (ab )) →4 a) = (ab)

Proof of Theorem ud4lem2
StepHypRef Expression
1 df-i4 47 . 2 ((a ∪ (ab )) →4 a) = ((((a ∪ (ab )) ∩ a) ∪ ((a ∪ (ab ))a)) ∪ (((a ∪ (ab ))a) ∩ a ))
2 ancom 74 . . . . . . 7 ((a ∪ (ab )) ∩ a) = (a ∩ (a ∪ (ab )))
3 anabs 121 . . . . . . 7 (a ∩ (a ∪ (ab ))) = a
42, 3ax-r2 36 . . . . . 6 ((a ∪ (ab )) ∩ a) = a
5 oran 87 . . . . . . . . 9 (a ∪ (ab )) = (a ∩ (ab ) )
65con2 67 . . . . . . . 8 (a ∪ (ab )) = (a ∩ (ab ) )
76ran 78 . . . . . . 7 ((a ∪ (ab ))a) = ((a ∩ (ab ) ) ∩ a)
8 ancom 74 . . . . . . . 8 ((a ∩ (ab ) ) ∩ a) = (a ∩ (a ∩ (ab ) ))
9 anass 76 . . . . . . . . . 10 ((aa ) ∩ (ab ) ) = (a ∩ (a ∩ (ab ) ))
109ax-r1 35 . . . . . . . . 9 (a ∩ (a ∩ (ab ) )) = ((aa ) ∩ (ab ) )
11 ancom 74 . . . . . . . . . 10 ((aa ) ∩ (ab ) ) = ((ab ) ∩ (aa ))
12 dff 101 . . . . . . . . . . . . 13 0 = (aa )
1312lan 77 . . . . . . . . . . . 12 ((ab ) ∩ 0) = ((ab ) ∩ (aa ))
1413ax-r1 35 . . . . . . . . . . 11 ((ab ) ∩ (aa )) = ((ab ) ∩ 0)
15 an0 108 . . . . . . . . . . 11 ((ab ) ∩ 0) = 0
1614, 15ax-r2 36 . . . . . . . . . 10 ((ab ) ∩ (aa )) = 0
1711, 16ax-r2 36 . . . . . . . . 9 ((aa ) ∩ (ab ) ) = 0
1810, 17ax-r2 36 . . . . . . . 8 (a ∩ (a ∩ (ab ) )) = 0
198, 18ax-r2 36 . . . . . . 7 ((a ∩ (ab ) ) ∩ a) = 0
207, 19ax-r2 36 . . . . . 6 ((a ∪ (ab ))a) = 0
214, 202or 72 . . . . 5 (((a ∪ (ab )) ∩ a) ∪ ((a ∪ (ab ))a)) = (a ∪ 0)
22 or0 102 . . . . 5 (a ∪ 0) = a
2321, 22ax-r2 36 . . . 4 (((a ∪ (ab )) ∩ a) ∪ ((a ∪ (ab ))a)) = a
24 ancom 74 . . . . 5 (((a ∪ (ab ))a) ∩ a ) = (a ∩ ((a ∪ (ab ))a))
25 oran 87 . . . . . . . . . . . . 13 (ab) = (ab )
2625ax-r1 35 . . . . . . . . . . . 12 (ab ) = (ab)
2726con3 68 . . . . . . . . . . 11 (ab ) = (ab)
2827lor 70 . . . . . . . . . 10 (a ∪ (ab )) = (a ∪ (ab) )
29 anor2 89 . . . . . . . . . . . 12 (a ∩ (ab)) = (a ∪ (ab) )
3029ax-r1 35 . . . . . . . . . . 11 (a ∪ (ab) ) = (a ∩ (ab))
3130con3 68 . . . . . . . . . 10 (a ∪ (ab) ) = (a ∩ (ab))
3228, 31ax-r2 36 . . . . . . . . 9 (a ∪ (ab )) = (a ∩ (ab))
3332con2 67 . . . . . . . 8 (a ∪ (ab )) = (a ∩ (ab))
3433ax-r5 38 . . . . . . 7 ((a ∪ (ab ))a) = ((a ∩ (ab)) ∪ a)
35 comid 187 . . . . . . . . . 10 a C a
3635comcom2 183 . . . . . . . . 9 a C a
37 comorr 184 . . . . . . . . 9 a C (ab)
3836, 37fh3r 475 . . . . . . . 8 ((a ∩ (ab)) ∪ a) = ((aa) ∩ ((ab) ∪ a))
39 ancom 74 . . . . . . . . . 10 ((aa) ∩ ((ab) ∪ a)) = (((ab) ∪ a) ∩ (aa))
40 or32 82 . . . . . . . . . . . 12 ((ab) ∪ a) = ((aa) ∪ b)
41 oridm 110 . . . . . . . . . . . . 13 (aa) = a
4241ax-r5 38 . . . . . . . . . . . 12 ((aa) ∪ b) = (ab)
4340, 42ax-r2 36 . . . . . . . . . . 11 ((ab) ∪ a) = (ab)
44 df-t 41 . . . . . . . . . . . . 13 1 = (aa )
45 ax-a2 31 . . . . . . . . . . . . 13 (aa ) = (aa)
4644, 45ax-r2 36 . . . . . . . . . . . 12 1 = (aa)
4746ax-r1 35 . . . . . . . . . . 11 (aa) = 1
4843, 472an 79 . . . . . . . . . 10 (((ab) ∪ a) ∩ (aa)) = ((ab) ∩ 1)
4939, 48ax-r2 36 . . . . . . . . 9 ((aa) ∩ ((ab) ∪ a)) = ((ab) ∩ 1)
50 an1 106 . . . . . . . . 9 ((ab) ∩ 1) = (ab)
5149, 50ax-r2 36 . . . . . . . 8 ((aa) ∩ ((ab) ∪ a)) = (ab)
5238, 51ax-r2 36 . . . . . . 7 ((a ∩ (ab)) ∪ a) = (ab)
5334, 52ax-r2 36 . . . . . 6 ((a ∪ (ab ))a) = (ab)
5453lan 77 . . . . 5 (a ∩ ((a ∪ (ab ))a)) = (a ∩ (ab))
5524, 54ax-r2 36 . . . 4 (((a ∪ (ab ))a) ∩ a ) = (a ∩ (ab))
5623, 552or 72 . . 3 ((((a ∪ (ab )) ∩ a) ∪ ((a ∪ (ab ))a)) ∪ (((a ∪ (ab ))a) ∩ a )) = (a ∪ (a ∩ (ab)))
57 oml 445 . . 3 (a ∪ (a ∩ (ab))) = (ab)
5856, 57ax-r2 36 . 2 ((((a ∪ (ab )) ∩ a) ∪ ((a ∪ (ab ))a)) ∪ (((a ∪ (ab ))a) ∩ a )) = (ab)
591, 58ax-r2 36 1 ((a ∪ (ab )) →4 a) = (ab)
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1wt 8  0wf 9  4 wi4 15
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud4  598
  Copyright terms: Public domain W3C validator