Proof of Theorem u1lem7
Step | Hyp | Ref
| Expression |
1 | | df-i1 44 |
. 2
(a →1 (a⊥ →1 b)) = (a⊥ ∪ (a ∩ (a⊥ →1 b))) |
2 | | ax-a1 30 |
. . . . . 6
a = a⊥
⊥ |
3 | 2 | ran 78 |
. . . . 5
(a ∩ (a⊥ →1 b)) = (a⊥ ⊥ ∩
(a⊥ →1
b)) |
4 | | ancom 74 |
. . . . . 6
(a⊥
⊥ ∩ (a⊥ →1 b)) = ((a⊥ →1 b) ∩ a⊥ ⊥
) |
5 | | u1lemana 605 |
. . . . . 6
((a⊥ →1
b) ∩ a⊥ ⊥ ) = a⊥
⊥ |
6 | 4, 5 | ax-r2 36 |
. . . . 5
(a⊥
⊥ ∩ (a⊥ →1 b)) = a⊥
⊥ |
7 | 3, 6 | ax-r2 36 |
. . . 4
(a ∩ (a⊥ →1 b)) = a⊥
⊥ |
8 | 7 | lor 70 |
. . 3
(a⊥ ∪ (a ∩ (a⊥ →1 b))) = (a⊥ ∪ a⊥ ⊥
) |
9 | | df-t 41 |
. . . 4
1 = (a⊥ ∪
a⊥ ⊥
) |
10 | 9 | ax-r1 35 |
. . 3
(a⊥ ∪ a⊥ ⊥ ) =
1 |
11 | 8, 10 | ax-r2 36 |
. 2
(a⊥ ∪ (a ∩ (a⊥ →1 b))) = 1 |
12 | 1, 11 | ax-r2 36 |
1
(a →1 (a⊥ →1 b)) = 1 |