Proof of Theorem u5lem4
Step | Hyp | Ref
| Expression |
1 | | u5lemc1 684 |
. . 3
a C (a →5 (b →5 a)) |
2 | 1 | u5lemc4 705 |
. 2
(a →5 (a →5 (b →5 a))) = (a⊥ ∪ (a →5 (b →5 a))) |
3 | | u5lem3 753 |
. . . 4
(a →5 (b →5 a)) = (a⊥ ∪ ((a ∩ b) ∪
(a ∩ b⊥ ))) |
4 | 3 | lor 70 |
. . 3
(a⊥ ∪ (a →5 (b →5 a))) = (a⊥ ∪ (a⊥ ∪ ((a ∩ b) ∪
(a ∩ b⊥ )))) |
5 | | ax-a3 32 |
. . . . 5
((a⊥ ∪ a⊥ ) ∪ ((a ∩ b) ∪
(a ∩ b⊥ ))) = (a⊥ ∪ (a⊥ ∪ ((a ∩ b) ∪
(a ∩ b⊥ )))) |
6 | 5 | ax-r1 35 |
. . . 4
(a⊥ ∪ (a⊥ ∪ ((a ∩ b) ∪
(a ∩ b⊥ )))) = ((a⊥ ∪ a⊥ ) ∪ ((a ∩ b) ∪
(a ∩ b⊥ ))) |
7 | | oridm 110 |
. . . . . 6
(a⊥ ∪ a⊥ ) = a⊥ |
8 | 7 | ax-r5 38 |
. . . . 5
((a⊥ ∪ a⊥ ) ∪ ((a ∩ b) ∪
(a ∩ b⊥ ))) = (a⊥ ∪ ((a ∩ b) ∪
(a ∩ b⊥ ))) |
9 | 3 | ax-r1 35 |
. . . . 5
(a⊥ ∪
((a ∩ b) ∪ (a
∩ b⊥ ))) = (a →5 (b →5 a)) |
10 | 8, 9 | ax-r2 36 |
. . . 4
((a⊥ ∪ a⊥ ) ∪ ((a ∩ b) ∪
(a ∩ b⊥ ))) = (a →5 (b →5 a)) |
11 | 6, 10 | ax-r2 36 |
. . 3
(a⊥ ∪ (a⊥ ∪ ((a ∩ b) ∪
(a ∩ b⊥ )))) = (a →5 (b →5 a)) |
12 | 4, 11 | ax-r2 36 |
. 2
(a⊥ ∪ (a →5 (b →5 a))) = (a
→5 (b →5
a)) |
13 | 2, 12 | ax-r2 36 |
1
(a →5 (a →5 (b →5 a))) = (a
→5 (b →5
a)) |