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

Theorem u3lemonb 637
 Description: Lemma for Kalmbach implication study.
Assertion
Ref Expression
u3lemonb ((a3 b) ∪ b ) = 1

Proof of Theorem u3lemonb
StepHypRef Expression
1 df-i3 46 . . 3 (a3 b) = (((ab) ∪ (ab )) ∪ (a ∩ (ab)))
21ax-r5 38 . 2 ((a3 b) ∪ b ) = ((((ab) ∪ (ab )) ∪ (a ∩ (ab))) ∪ b )
3 or32 82 . . 3 ((((ab) ∪ (ab )) ∪ (a ∩ (ab))) ∪ b ) = ((((ab) ∪ (ab )) ∪ b ) ∪ (a ∩ (ab)))
4 ax-a3 32 . . . . . 6 (((ab) ∪ (ab )) ∪ b ) = ((ab) ∪ ((ab ) ∪ b ))
5 lear 161 . . . . . . . 8 (ab ) ≤ b
65df-le2 131 . . . . . . 7 ((ab ) ∪ b ) = b
76lor 70 . . . . . 6 ((ab) ∪ ((ab ) ∪ b )) = ((ab) ∪ b )
84, 7ax-r2 36 . . . . 5 (((ab) ∪ (ab )) ∪ b ) = ((ab) ∪ b )
9 ancom 74 . . . . 5 (a ∩ (ab)) = ((ab) ∩ a)
108, 92or 72 . . . 4 ((((ab) ∪ (ab )) ∪ b ) ∪ (a ∩ (ab))) = (((ab) ∪ b ) ∪ ((ab) ∩ a))
11 comor1 461 . . . . . . . 8 (ab) C a
12 comor2 462 . . . . . . . 8 (ab) C b
1311, 12com2an 484 . . . . . . 7 (ab) C (ab)
1412comcom2 183 . . . . . . 7 (ab) C b
1513, 14com2or 483 . . . . . 6 (ab) C ((ab) ∪ b )
1611comcom7 460 . . . . . 6 (ab) C a
1715, 16fh4 472 . . . . 5 (((ab) ∪ b ) ∪ ((ab) ∩ a)) = ((((ab) ∪ b ) ∪ (ab)) ∩ (((ab) ∪ b ) ∪ a))
18 ax-a3 32 . . . . . . . 8 (((ab) ∪ b ) ∪ (ab)) = ((ab) ∪ (b ∪ (ab)))
19 ax-a2 31 . . . . . . . . . . 11 (b ∪ (ab)) = ((ab) ∪ b )
20 ax-a3 32 . . . . . . . . . . . 12 ((ab) ∪ b ) = (a ∪ (bb ))
21 df-t 41 . . . . . . . . . . . . . . 15 1 = (bb )
2221ax-r1 35 . . . . . . . . . . . . . 14 (bb ) = 1
2322lor 70 . . . . . . . . . . . . 13 (a ∪ (bb )) = (a ∪ 1)
24 or1 104 . . . . . . . . . . . . 13 (a ∪ 1) = 1
2523, 24ax-r2 36 . . . . . . . . . . . 12 (a ∪ (bb )) = 1
2620, 25ax-r2 36 . . . . . . . . . . 11 ((ab) ∪ b ) = 1
2719, 26ax-r2 36 . . . . . . . . . 10 (b ∪ (ab)) = 1
2827lor 70 . . . . . . . . 9 ((ab) ∪ (b ∪ (ab))) = ((ab) ∪ 1)
29 or1 104 . . . . . . . . 9 ((ab) ∪ 1) = 1
3028, 29ax-r2 36 . . . . . . . 8 ((ab) ∪ (b ∪ (ab))) = 1
3118, 30ax-r2 36 . . . . . . 7 (((ab) ∪ b ) ∪ (ab)) = 1
32 ax-a3 32 . . . . . . . 8 (((ab) ∪ b ) ∪ a) = ((ab) ∪ (ba))
33 ancom 74 . . . . . . . . . . . . 13 (ab) = (ba )
34 anor1 88 . . . . . . . . . . . . 13 (ba ) = (ba)
3533, 34ax-r2 36 . . . . . . . . . . . 12 (ab) = (ba)
3635con2 67 . . . . . . . . . . 11 (ab) = (ba)
3736ax-r1 35 . . . . . . . . . 10 (ba) = (ab)
3837lor 70 . . . . . . . . 9 ((ab) ∪ (ba)) = ((ab) ∪ (ab) )
39 df-t 41 . . . . . . . . . 10 1 = ((ab) ∪ (ab) )
4039ax-r1 35 . . . . . . . . 9 ((ab) ∪ (ab) ) = 1
4138, 40ax-r2 36 . . . . . . . 8 ((ab) ∪ (ba)) = 1
4232, 41ax-r2 36 . . . . . . 7 (((ab) ∪ b ) ∪ a) = 1
4331, 422an 79 . . . . . 6 ((((ab) ∪ b ) ∪ (ab)) ∩ (((ab) ∪ b ) ∪ a)) = (1 ∩ 1)
44 an1 106 . . . . . 6 (1 ∩ 1) = 1
4543, 44ax-r2 36 . . . . 5 ((((ab) ∪ b ) ∪ (ab)) ∩ (((ab) ∪ b ) ∪ a)) = 1
4617, 45ax-r2 36 . . . 4 (((ab) ∪ b ) ∪ ((ab) ∩ a)) = 1
4710, 46ax-r2 36 . . 3 ((((ab) ∪ (ab )) ∪ b ) ∪ (a ∩ (ab))) = 1
483, 47ax-r2 36 . 2 ((((ab) ∪ (ab )) ∪ (a ∩ (ab))) ∪ b ) = 1
492, 48ax-r2 36 1 ((a3 b) ∪ b ) = 1
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →3 wi3 14 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-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133 This theorem is referenced by:  u3lemnab  652  u3lem3  751  u3lem4  758
 Copyright terms: Public domain W3C validator