Proof of Theorem wql2lem3
Step | Hyp | Ref
| Expression |
1 | | df-i2 45 |
. 2
((a ∩ b⊥ ) →2 a⊥ ) = (a⊥ ∪ ((a ∩ b⊥ )⊥ ∩
a⊥ ⊥
)) |
2 | | oran2 92 |
. . . . . 6
(a⊥ ∪ b) = (a ∩
b⊥
)⊥ |
3 | 2 | ax-r1 35 |
. . . . 5
(a ∩ b⊥ )⊥ = (a⊥ ∪ b) |
4 | 3 | ran 78 |
. . . 4
((a ∩ b⊥ )⊥ ∩
a⊥ ⊥ ) =
((a⊥ ∪ b) ∩ a⊥ ⊥
) |
5 | | ancom 74 |
. . . 4
((a⊥ ∪ b) ∩ a⊥ ⊥ ) = (a⊥ ⊥ ∩
(a⊥ ∪ b)) |
6 | 4, 5 | ax-r2 36 |
. . 3
((a ∩ b⊥ )⊥ ∩
a⊥ ⊥ ) =
(a⊥ ⊥
∩ (a⊥ ∪ b)) |
7 | 6 | lor 70 |
. 2
(a⊥ ∪
((a ∩ b⊥ )⊥ ∩
a⊥ ⊥ )) =
(a⊥ ∪ (a⊥ ⊥ ∩
(a⊥ ∪ b))) |
8 | | wql2lem3.1 |
. . . 4
(a →2 b) = 1 |
9 | 8 | wql2lem 288 |
. . 3
(a⊥ ∪ b) = 1 |
10 | | omlem2 128 |
. . 3
((a⊥ ∪ b)⊥ ∪ (a⊥ ∪ (a⊥ ⊥ ∩
(a⊥ ∪ b)))) = 1 |
11 | 9, 10 | skr0 242 |
. 2
(a⊥ ∪ (a⊥ ⊥ ∩
(a⊥ ∪ b))) = 1 |
12 | 1, 7, 11 | 3tr 65 |
1
((a ∩ b⊥ ) →2 a⊥ ) = 1 |