[Lattice L46-7]Home PageHome Quantum Logic Explorer < Previous   Next >
Related theorems
GIF version
Theorem u3lem13b 772
Description: Lemma for unified implication study.
Assertion
Ref Expression
u3lem13b ((a →3 b⊥ ) →3 a⊥ ) = (a →1 b)
Proof of Theorem u3lem13b
StepHypRef Expression
1 df-i3 45 . 2 ((a →3 b⊥ ) →3 a⊥ ) = ((((a →3 b⊥ )⊥ ∩ a⊥ ) ∪ ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ )) ∪ ((a →3 b⊥ ) ∩ ((a →3 b⊥ )⊥ ∪ a⊥ )))
2 u3lemnana 629 . . . . . 6 ((a →3 b⊥ )⊥ ∩ a⊥ ) = (a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
3 ax-a1 29 . . . . . . . . 9 a = a⊥ ⊥
43ax-r1 34 . . . . . . . 8 a⊥ ⊥ = a
54lan 70 . . . . . . 7 ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ ) = ((a →3 b⊥ )⊥ ∩ a)
6 u3lemnaa 624 . . . . . . 7 ((a →3 b⊥ )⊥ ∩ a) = (a ∩ b⊥ ⊥ )
75, 6ax-r2 35 . . . . . 6 ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ ) = (a ∩ b⊥ ⊥ )
82, 72or 67 . . . . 5 (((a →3 b⊥ )⊥ ∩ a⊥ ) ∪ ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ )) = ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ (a ∩ b⊥ ⊥ ))
9 comanr1 446 . . . . . . . 8 a C (a ∩ b⊥ ⊥ )
109comcom3 436 . . . . . . 7 a⊥ C (a ∩ b⊥ ⊥ )
11 comorr 176 . . . . . . . . 9 a C (a ∪ b⊥ )
12 comorr 176 . . . . . . . . 9 a C (a ∪ b⊥ ⊥ )
1311, 12com2an 466 . . . . . . . 8 a C ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
1413comcom3 436 . . . . . . 7 a⊥ C ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
1510, 14fh4r 458 . . . . . 6 ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ (a ∩ b⊥ ⊥ )) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ (a ∩ b⊥ ⊥ )))
16 coman1 177 . . . . . . . . . 10 (a ∩ b⊥ ⊥ ) C a
17 coman2 178 . . . . . . . . . . 11 (a ∩ b⊥ ⊥ ) C b⊥ ⊥
1817comcom7 442 . . . . . . . . . 10 (a ∩ b⊥ ⊥ ) C b⊥
1916, 18com2or 465 . . . . . . . . 9 (a ∩ b⊥ ⊥ ) C (a ∪ b⊥ )
2016, 17com2or 465 . . . . . . . . 9 (a ∩ b⊥ ⊥ ) C (a ∪ b⊥ ⊥ )
2119, 20fh3r 457 . . . . . . . 8 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ (a ∩ b⊥ ⊥ )) = (((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ )))
2221lan 70 . . . . . . 7 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ (a ∩ b⊥ ⊥ ))) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ (((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ ))))
23 ax-a2 30 . . . . . . . . . . . 12 ((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) = ((a ∩ b⊥ ⊥ ) ∪ (a ∪ b⊥ ))
24 lea 152 . . . . . . . . . . . . . 14 (a ∩ b⊥ ⊥ ) ≤ a
25 leo 150 . . . . . . . . . . . . . 14 a ≤ (a ∪ b⊥ )
2624, 25letr 129 . . . . . . . . . . . . 13 (a ∩ b⊥ ⊥ ) ≤ (a ∪ b⊥ )
2726df-le2 123 . . . . . . . . . . . 12 ((a ∩ b⊥ ⊥ ) ∪ (a ∪ b⊥ )) = (a ∪ b⊥ )
2823, 27ax-r2 35 . . . . . . . . . . 11 ((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) = (a ∪ b⊥ )
29 ax-a2 30 . . . . . . . . . . . 12 ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ )) = ((a ∩ b⊥ ⊥ ) ∪ (a ∪ b⊥ ⊥ ))
30 leo 150 . . . . . . . . . . . . . 14 a ≤ (a ∪ b⊥ ⊥ )
3124, 30letr 129 . . . . . . . . . . . . 13 (a ∩ b⊥ ⊥ ) ≤ (a ∪ b⊥ ⊥ )
3231df-le2 123 . . . . . . . . . . . 12 ((a ∩ b⊥ ⊥ ) ∪ (a ∪ b⊥ ⊥ )) = (a ∪ b⊥ ⊥ )
3329, 32ax-r2 35 . . . . . . . . . . 11 ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ )) = (a ∪ b⊥ ⊥ )
3428, 332an 72 . . . . . . . . . 10 (((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ ))) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
35 id 58 . . . . . . . . . 10 ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
3634, 35ax-r2 35 . . . . . . . . 9 (((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ ))) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
3736lan 70 . . . . . . . 8 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ (((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ )))) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
38 id 58 . . . . . . . 8 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
3937, 38ax-r2 35 . . . . . . 7 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ (((a ∪ b⊥ ) ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ⊥ ) ∪ (a ∩ b⊥ ⊥ )))) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
4022, 39ax-r2 35 . . . . . 6 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ (a ∩ b⊥ ⊥ ))) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
4115, 40ax-r2 35 . . . . 5 ((a⊥ ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ (a ∩ b⊥ ⊥ )) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
428, 41ax-r2 35 . . . 4 (((a →3 b⊥ )⊥ ∩ a⊥ ) ∪ ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ )) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )))
43 u3lemnona 649 . . . . . 6 ((a →3 b⊥ )⊥ ∪ a⊥ ) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
4443lan 70 . . . . 5 ((a →3 b⊥ ) ∩ ((a →3 b⊥ )⊥ ∪ a⊥ )) = ((a →3 b⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ ⊥ )))
45 comi31 490 . . . . . . . 8 a C (a →3 b⊥ )
4645comcom3 436 . . . . . . 7 a⊥ C (a →3 b⊥ )
4746, 10fh2 452 . . . . . 6 ((a →3 b⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ ⊥ ))) = (((a →3 b⊥ ) ∩ a⊥ ) ∪ ((a →3 b⊥ ) ∩ (a ∩ b⊥ ⊥ )))
48 u3lemana 589 . . . . . . . 8 ((a →3 b⊥ ) ∩ a⊥ ) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
49 anandi 106 . . . . . . . . 9 ((a →3 b⊥ ) ∩ (a ∩ b⊥ ⊥ )) = (((a →3 b⊥ ) ∩ a) ∩ ((a →3 b⊥ ) ∩ b⊥ ⊥ ))
50 u3lemaa 584 . . . . . . . . . . 11 ((a →3 b⊥ ) ∩ a) = (a ∩ (a⊥ ∪ b⊥ ))
51 u3lemanb 599 . . . . . . . . . . 11 ((a →3 b⊥ ) ∩ b⊥ ⊥ ) = (a⊥ ∩ b⊥ ⊥ )
5250, 512an 72 . . . . . . . . . 10 (((a →3 b⊥ ) ∩ a) ∩ ((a →3 b⊥ ) ∩ b⊥ ⊥ )) = ((a ∩ (a⊥ ∪ b⊥ )) ∩ (a⊥ ∩ b⊥ ⊥ ))
53 an4 78 . . . . . . . . . . 11 ((a ∩ (a⊥ ∪ b⊥ )) ∩ (a⊥ ∩ b⊥ ⊥ )) = ((a ∩ a⊥ ) ∩ ((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ ))
54 ancom 68 . . . . . . . . . . . 12 ((a ∩ a⊥ ) ∩ ((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ )) = (((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ ) ∩ (a ∩ a⊥ ))
55 dff 93 . . . . . . . . . . . . . . 15 0 = (a ∩ a⊥ )
5655ax-r1 34 . . . . . . . . . . . . . 14 (a ∩ a⊥ ) = 0
5756lan 70 . . . . . . . . . . . . 13 (((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ ) ∩ (a ∩ a⊥ )) = (((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ ) ∩ 0)
58 an0 100 . . . . . . . . . . . . 13 (((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ ) ∩ 0) = 0
5957, 58ax-r2 35 . . . . . . . . . . . 12 (((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ ) ∩ (a ∩ a⊥ )) = 0
6054, 59ax-r2 35 . . . . . . . . . . 11 ((a ∩ a⊥ ) ∩ ((a⊥ ∪ b⊥ ) ∩ b⊥ ⊥ )) = 0
6153, 60ax-r2 35 . . . . . . . . . 10 ((a ∩ (a⊥ ∪ b⊥ )) ∩ (a⊥ ∩ b⊥ ⊥ )) = 0
6252, 61ax-r2 35 . . . . . . . . 9 (((a →3 b⊥ ) ∩ a) ∩ ((a →3 b⊥ ) ∩ b⊥ ⊥ )) = 0
6349, 62ax-r2 35 . . . . . . . 8 ((a →3 b⊥ ) ∩ (a ∩ b⊥ ⊥ )) = 0
6448, 632or 67 . . . . . . 7 (((a →3 b⊥ ) ∩ a⊥ ) ∪ ((a →3 b⊥ ) ∩ (a ∩ b⊥ ⊥ ))) = (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ 0)
65 or0 94 . . . . . . 7 (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ 0) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
6664, 65ax-r2 35 . . . . . 6 (((a →3 b⊥ ) ∩ a⊥ ) ∪ ((a →3 b⊥ ) ∩ (a ∩ b⊥ ⊥ ))) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
6747, 66ax-r2 35 . . . . 5 ((a →3 b⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ ⊥ ))) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
6844, 67ax-r2 35 . . . 4 ((a →3 b⊥ ) ∩ ((a →3 b⊥ )⊥ ∪ a⊥ )) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
6942, 682or 67 . . 3 ((((a →3 b⊥ )⊥ ∩ a⊥ ) ∪ ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ )) ∪ ((a →3 b⊥ ) ∩ ((a →3 b⊥ )⊥ ∪ a⊥ ))) = (((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )))
70 comanr1 446 . . . . . . . . 9 a⊥ C (a⊥ ∩ b⊥ )
71 comanr1 446 . . . . . . . . 9 a⊥ C (a⊥ ∩ b⊥ ⊥ )
7270, 71com2or 465 . . . . . . . 8 a⊥ C ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
7372comcom 435 . . . . . . 7 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) C a⊥
7473comcom7 442 . . . . . . . 8 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) C a
75 comanr2 447 . . . . . . . . . . 11 b⊥ C (a⊥ ∩ b⊥ )
7675comcom3 436 . . . . . . . . . 10 b⊥ ⊥ C (a⊥ ∩ b⊥ )
77 comanr2 447 . . . . . . . . . 10 b⊥ ⊥ C (a⊥ ∩ b⊥ ⊥ )
7876, 77com2or 465 . . . . . . . . 9 b⊥ ⊥ C ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
7978comcom 435 . . . . . . . 8 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) C b⊥ ⊥
8074, 79com2an 466 . . . . . . 7 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) C (a ∩ b⊥ ⊥ )
8173, 80com2or 465 . . . . . 6 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) C (a⊥ ∪ (a ∩ b⊥ ⊥ ))
8281comcom 435 . . . . 5 (a⊥ ∪ (a ∩ b⊥ ⊥ )) C ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
8313comcom 435 . . . . . . . 8 ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) C a
8483comcom2 175 . . . . . . 7 ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) C a⊥
85 comorr2 445 . . . . . . . . . . 11 b⊥ C (a ∪ b⊥ )
8685comcom3 436 . . . . . . . . . 10 b⊥ ⊥ C (a ∪ b⊥ )
87 comorr2 445 . . . . . . . . . 10 b⊥ ⊥ C (a ∪ b⊥ ⊥ )
8886, 87com2an 466 . . . . . . . . 9 b⊥ ⊥ C ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
8988comcom 435 . . . . . . . 8 ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) C b⊥ ⊥
9083, 89com2an 466 . . . . . . 7 ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) C (a ∩ b⊥ ⊥ )
9184, 90com2or 465 . . . . . 6 ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) C (a⊥ ∪ (a ∩ b⊥ ⊥ ))
9291comcom 435 . . . . 5 (a⊥ ∪ (a ∩ b⊥ ⊥ )) C ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))
9382, 92fh4r 458 . . . 4 (((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))))
94 ax-a2 30 . . . . . . 7 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ (a⊥ ∪ (a ∩ b⊥ ⊥ )))
95 lea 152 . . . . . . . . . . 11 (a⊥ ∩ b⊥ ) ≤ a⊥
96 lea 152 . . . . . . . . . . 11 (a⊥ ∩ b⊥ ⊥ ) ≤ a⊥
9795, 96lel2or 162 . . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ≤ a⊥
98 leo 150 . . . . . . . . . 10 a⊥ ≤ (a⊥ ∪ (a ∩ b⊥ ⊥ ))
9997, 98letr 129 . . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ≤ (a⊥ ∪ (a ∩ b⊥ ⊥ ))
10099df-le2 123 . . . . . . . 8 (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ (a⊥ ∪ (a ∩ b⊥ ⊥ ))) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
101 id 58 . . . . . . . 8 (a⊥ ∪ (a ∩ b⊥ ⊥ )) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
102100, 101ax-r2 35 . . . . . . 7 (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ (a⊥ ∪ (a ∩ b⊥ ⊥ ))) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
10394, 102ax-r2 35 . . . . . 6 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
104 ax-a2 30 . . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) = ((a⊥ ∩ b⊥ ⊥ ) ∪ (a⊥ ∩ b⊥ ))
105 anor3 82 . . . . . . . . . . 11 (a⊥ ∩ b⊥ ⊥ ) = (a ∪ b⊥ )⊥
106 anor2 81 . . . . . . . . . . 11 (a⊥ ∩ b⊥ ) = (a ∪ b⊥ ⊥ )⊥
107105, 1062or 67 . . . . . . . . . 10 ((a⊥ ∩ b⊥ ⊥ ) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b⊥ )⊥ ∪ (a ∪ b⊥ ⊥ )⊥ )
108 oran3 85 . . . . . . . . . 10 ((a ∪ b⊥ )⊥ ∪ (a ∪ b⊥ ⊥ )⊥ ) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥
109107, 108ax-r2 35 . . . . . . . . 9 ((a⊥ ∩ b⊥ ⊥ ) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥
110104, 109ax-r2 35 . . . . . . . 8 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) = ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥
111110lor 66 . . . . . . 7 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥ )
112 df-t 40 . . . . . . . 8 1 = (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥ )
113112ax-r1 34 . . . . . . 7 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))⊥ ) = 1
114111, 113ax-r2 35 . . . . . 6 (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = 1
115103, 1142an 72 . . . . 5 (((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )))) = ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ 1)
116 an1 98 . . . . . 6 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ 1) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
117 df-i1 43 . . . . . . . 8 (a →1 b⊥ ⊥ ) = (a⊥ ∪ (a ∩ b⊥ ⊥ ))
118117ax-r1 34 . . . . . . 7 (a⊥ ∪ (a ∩ b⊥ ⊥ )) = (a →1 b⊥ ⊥ )
119 ax-a1 29 . . . . . . . . 9 b = b⊥ ⊥
120119ax-r1 34 . . . . . . . 8 b⊥ ⊥ = b
121120ud1lem0a 247 . . . . . . 7 (a →1 b⊥ ⊥ ) = (a →1 b)
122118, 121ax-r2 35 . . . . . 6 (a⊥ ∪ (a ∩ b⊥ ⊥ )) = (a →1 b)
123116, 122ax-r2 35 . . . . 5 ((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ 1) = (a →1 b)
124115, 123ax-r2 35 . . . 4 (((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) ∩ (((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )))) = (a →1 b)
12593, 124ax-r2 35 . . 3 (((a⊥ ∪ (a ∩ b⊥ ⊥ )) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b⊥ ⊥ ))) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))) = (a →1 b)
12669, 125ax-r2 35 . 2 ((((a →3 b⊥ )⊥ ∩ a⊥ ) ∪ ((a →3 b⊥ )⊥ ∩ a⊥ ⊥ )) ∪ ((a →3 b⊥ ) ∩ ((a →3 b⊥ )⊥ ∪ a⊥ ))) = (a →1 b)
1271, 126ax-r2 35 1 ((a →3 b⊥ ) →3 a⊥ ) = (a →1 b)
Colors of variables: term
Syntax hints:   = wb 1  ⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 9  0wf 10   →1 wi1 13   →3 wi3 15
This theorem is referenced by:  u3lem14a 773  u3lem14aa2 775
This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421
This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i3 45  df-le1 122  df-le2 123  df-c1 124  df-c2 125
metamath.org