Proof of Theorem 2oath1
Step | Hyp | Ref
| Expression |
1 | | df-i2 45 |
. . 3
((b ∪ c) →2 ((a →2 b) ∩ (a
→2 c))) = (((a →2 b) ∩ (a
→2 c)) ∪ ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
)) |
2 | 1 | lan 77 |
. 2
((a →2 b) ∩ ((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c)))) = ((a →2 b) ∩ (((a
→2 b) ∩ (a →2 c)) ∪ ((b
∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
))) |
3 | | coman1 185 |
. . 3
((a →2 b) ∩ (a
→2 c)) C (a →2 b) |
4 | | comorr2 463 |
. . . . 5
((a →2 b) ∩ (a
→2 c)) C ((b ∪ c) ∪
((a →2 b) ∩ (a
→2 c))) |
5 | 4 | comcom2 183 |
. . . 4
((a →2 b) ∩ (a
→2 c)) C ((b ∪ c) ∪
((a →2 b) ∩ (a
→2 c)))⊥ |
6 | | anor3 90 |
. . . . 5
((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥ )
= ((b ∪ c) ∪ ((a
→2 b) ∩ (a →2 c)))⊥ |
7 | 6 | ax-r1 35 |
. . . 4
((b ∪ c) ∪ ((a
→2 b) ∩ (a →2 c)))⊥ = ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
) |
8 | 5, 7 | cbtr 182 |
. . 3
((a →2 b) ∩ (a
→2 c)) C ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
) |
9 | 3, 8 | fh2 470 |
. 2
((a →2 b) ∩ (((a
→2 b) ∩ (a →2 c)) ∪ ((b
∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
))) = (((a →2 b) ∩ ((a
→2 b) ∩ (a →2 c))) ∪ ((a
→2 b) ∩ ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
))) |
10 | | anass 76 |
. . . . . 6
(((a →2 b) ∩ (a
→2 b)) ∩ (a →2 c)) = ((a
→2 b) ∩ ((a →2 b) ∩ (a
→2 c))) |
11 | 10 | ax-r1 35 |
. . . . 5
((a →2 b) ∩ ((a
→2 b) ∩ (a →2 c))) = (((a
→2 b) ∩ (a →2 b)) ∩ (a
→2 c)) |
12 | | anidm 111 |
. . . . . 6
((a →2 b) ∩ (a
→2 b)) = (a →2 b) |
13 | 12 | ran 78 |
. . . . 5
(((a →2 b) ∩ (a
→2 b)) ∩ (a →2 c)) = ((a
→2 b) ∩ (a →2 c)) |
14 | 11, 13 | ax-r2 36 |
. . . 4
((a →2 b) ∩ ((a
→2 b) ∩ (a →2 c))) = ((a
→2 b) ∩ (a →2 c)) |
15 | | oran 87 |
. . . . . . . . 9
((b ∪ c) ∪ ((a
→2 b) ∩ (a →2 c))) = ((b ∪
c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
)⊥ |
16 | 15 | lor 70 |
. . . . . . . 8
((a →2 b)⊥ ∪ ((b ∪ c) ∪
((a →2 b) ∩ (a
→2 c)))) = ((a →2 b)⊥ ∪ ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
)⊥ ) |
17 | 16 | ax-r1 35 |
. . . . . . 7
((a →2 b)⊥ ∪ ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
)⊥ ) = ((a →2
b)⊥ ∪ ((b ∪ c) ∪
((a →2 b) ∩ (a
→2 c)))) |
18 | | 2oalem1 825 |
. . . . . . 7
((a →2 b)⊥ ∪ ((b ∪ c) ∪
((a →2 b) ∩ (a
→2 c)))) =
1 |
19 | 17, 18 | ax-r2 36 |
. . . . . 6
((a →2 b)⊥ ∪ ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
)⊥ ) = 1 |
20 | 19 | ax-r4 37 |
. . . . 5
((a →2 b)⊥ ∪ ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
)⊥ )⊥ = 1⊥ |
21 | | df-a 40 |
. . . . 5
((a →2 b) ∩ ((b
∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥ ))
= ((a →2 b)⊥ ∪ ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
)⊥ )⊥ |
22 | | df-f 42 |
. . . . 5
0 = 1⊥ |
23 | 20, 21, 22 | 3tr1 63 |
. . . 4
((a →2 b) ∩ ((b
∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥ ))
= 0 |
24 | 14, 23 | 2or 72 |
. . 3
(((a →2 b) ∩ ((a
→2 b) ∩ (a →2 c))) ∪ ((a
→2 b) ∩ ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
))) = (((a →2 b) ∩ (a
→2 c)) ∪
0) |
25 | | or0 102 |
. . 3
(((a →2 b) ∩ (a
→2 c)) ∪ 0) =
((a →2 b) ∩ (a
→2 c)) |
26 | 24, 25 | ax-r2 36 |
. 2
(((a →2 b) ∩ ((a
→2 b) ∩ (a →2 c))) ∪ ((a
→2 b) ∩ ((b ∪ c)⊥ ∩ ((a →2 b) ∩ (a
→2 c))⊥
))) = ((a →2 b) ∩ (a
→2 c)) |
27 | 2, 9, 26 | 3tr 65 |
1
((a →2 b) ∩ ((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c)))) = ((a →2 b) ∩ (a
→2 c)) |