Proof of Theorem oa3-1lem
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ancom 74 |
. 2
(1 ∩ (0 ∪ (a ∩ (((0
∩ a) ∪ (1 ∩ (a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))))))) = ((0 ∪
(a ∩ (((0 ∩ a) ∪ (1 ∩ (a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c))))))) ∩
1) |
| 2 | | an1 106 |
. 2
((0 ∪ (a ∩ (((0 ∩
a) ∪ (1 ∩ (a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c))))))) ∩ 1) = (0
∪ (a ∩ (((0 ∩ a) ∪ (1 ∩ (a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c))))))) |
| 3 | | ax-a2 31 |
. . 3
(0 ∪ (a ∩ (((0 ∩
a) ∪ (1 ∩ (a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c))))))) = ((a ∩ (((0 ∩ a) ∪ (1 ∩ (a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))))) ∪
0) |
| 4 | | or0 102 |
. . 3
((a ∩ (((0 ∩ a) ∪ (1 ∩ (a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))))) ∪ 0) =
(a ∩ (((0 ∩ a) ∪ (1 ∩ (a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))))) |
| 5 | | ancom 74 |
. . . . . . . . 9
(0 ∩ a) = (a ∩ 0) |
| 6 | | an0 108 |
. . . . . . . . 9
(a ∩ 0) = 0 |
| 7 | 5, 6 | ax-r2 36 |
. . . . . . . 8
(0 ∩ a) = 0 |
| 8 | | ancom 74 |
. . . . . . . . 9
(1 ∩ (a →1
c)) = ((a →1 c) ∩ 1) |
| 9 | | an1 106 |
. . . . . . . . 9
((a →1 c) ∩ 1) = (a
→1 c) |
| 10 | 8, 9 | ax-r2 36 |
. . . . . . . 8
(1 ∩ (a →1
c)) = (a →1 c) |
| 11 | 7, 10 | 2or 72 |
. . . . . . 7
((0 ∩ a) ∪ (1 ∩
(a →1 c))) = (0 ∪ (a →1 c)) |
| 12 | | ax-a2 31 |
. . . . . . 7
(0 ∪ (a →1
c)) = ((a →1 c) ∪ 0) |
| 13 | | or0 102 |
. . . . . . 7
((a →1 c) ∪ 0) = (a
→1 c) |
| 14 | 11, 12, 13 | 3tr 65 |
. . . . . 6
((0 ∩ a) ∪ (1 ∩
(a →1 c))) = (a
→1 c) |
| 15 | 14 | ax-r5 38 |
. . . . 5
(((0 ∩ a) ∪ (1 ∩
(a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c))))) = ((a →1 c) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c))))) |
| 16 | | ax-a2 31 |
. . . . . . . 8
((0 ∩ b) ∪ (1 ∩
(b →1 c))) = ((1 ∩ (b →1 c)) ∪ (0 ∩ b)) |
| 17 | | ancom 74 |
. . . . . . . . . 10
(1 ∩ (b →1
c)) = ((b →1 c) ∩ 1) |
| 18 | | an1 106 |
. . . . . . . . . 10
((b →1 c) ∩ 1) = (b
→1 c) |
| 19 | 17, 18 | ax-r2 36 |
. . . . . . . . 9
(1 ∩ (b →1
c)) = (b →1 c) |
| 20 | | ancom 74 |
. . . . . . . . . 10
(0 ∩ b) = (b ∩ 0) |
| 21 | | an0 108 |
. . . . . . . . . 10
(b ∩ 0) = 0 |
| 22 | 20, 21 | ax-r2 36 |
. . . . . . . . 9
(0 ∩ b) = 0 |
| 23 | 19, 22 | 2or 72 |
. . . . . . . 8
((1 ∩ (b →1
c)) ∪ (0 ∩ b)) = ((b
→1 c) ∪
0) |
| 24 | | or0 102 |
. . . . . . . 8
((b →1 c) ∪ 0) = (b
→1 c) |
| 25 | 16, 23, 24 | 3tr 65 |
. . . . . . 7
((0 ∩ b) ∪ (1 ∩
(b →1 c))) = (b
→1 c) |
| 26 | 25 | ran 78 |
. . . . . 6
(((0 ∩ b) ∪ (1 ∩
(b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))) = ((b →1 c) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))) |
| 27 | 26 | lor 70 |
. . . . 5
((a →1 c) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c))))) = ((a →1 c) ∪ ((b
→1 c) ∩ ((a ∩ b) ∪
((a →1 c) ∩ (b
→1 c))))) |
| 28 | 15, 27 | ax-r2 36 |
. . . 4
(((0 ∩ a) ∪ (1 ∩
(a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c))))) = ((a →1 c) ∪ ((b
→1 c) ∩ ((a ∩ b) ∪
((a →1 c) ∩ (b
→1 c))))) |
| 29 | 28 | lan 77 |
. . 3
(a ∩ (((0 ∩ a) ∪ (1 ∩ (a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))))) = (a ∩ ((a
→1 c) ∪ ((b →1 c) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))))) |
| 30 | 3, 4, 29 | 3tr 65 |
. 2
(0 ∪ (a ∩ (((0 ∩
a) ∪ (1 ∩ (a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c))))))) = (a ∩ ((a
→1 c) ∪ ((b →1 c) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))))) |
| 31 | 1, 2, 30 | 3tr 65 |
1
(1 ∩ (0 ∪ (a ∩ (((0
∩ a) ∪ (1 ∩ (a →1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b →1 c))) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))))))) = (a ∩ ((a
→1 c) ∪ ((b →1 c) ∩ ((a
∩ b) ∪ ((a →1 c) ∩ (b
→1 c)))))) |
