Proof of Theorem u1lem2
Step | Hyp | Ref
| Expression |
1 | | df-i1 44 |
. 2
(((a →1 b) →1 a) →1 a) = (((a
→1 b) →1
a)⊥ ∪
(((a →1 b) →1 a) ∩ a)) |
2 | | u1lem1n 739 |
. . . 4
((a →1 b) →1 a)⊥ = a⊥ |
3 | | u1lem1 734 |
. . . . . 6
((a →1 b) →1 a) = a |
4 | 3 | ran 78 |
. . . . 5
(((a →1 b) →1 a) ∩ a) =
(a ∩ a) |
5 | | anidm 111 |
. . . . 5
(a ∩ a) = a |
6 | 4, 5 | ax-r2 36 |
. . . 4
(((a →1 b) →1 a) ∩ a) =
a |
7 | 2, 6 | 2or 72 |
. . 3
(((a →1 b) →1 a)⊥ ∪ (((a →1 b) →1 a) ∩ a)) =
(a⊥ ∪ a) |
8 | | ax-a2 31 |
. . . 4
(a⊥ ∪ a) = (a ∪
a⊥ ) |
9 | | df-t 41 |
. . . . 5
1 = (a ∪ a⊥ ) |
10 | 9 | ax-r1 35 |
. . . 4
(a ∪ a⊥ ) = 1 |
11 | 8, 10 | ax-r2 36 |
. . 3
(a⊥ ∪ a) = 1 |
12 | 7, 11 | ax-r2 36 |
. 2
(((a →1 b) →1 a)⊥ ∪ (((a →1 b) →1 a) ∩ a)) =
1 |
13 | 1, 12 | ax-r2 36 |
1
(((a →1 b) →1 a) →1 a) = 1 |