Proof of Theorem 2vwomr2
Step | Hyp | Ref
| Expression |
1 | | ancom 74 |
. . . 4
(a ∩ b) = (b ∩
a) |
2 | | ax-a1 30 |
. . . . 5
b = b⊥
⊥ |
3 | | ax-a1 30 |
. . . . 5
a = a⊥
⊥ |
4 | 2, 3 | 2an 79 |
. . . 4
(b ∩ a) = (b⊥ ⊥ ∩
a⊥ ⊥
) |
5 | 1, 4 | ax-r2 36 |
. . 3
(a ∩ b) = (b⊥ ⊥ ∩
a⊥ ⊥
) |
6 | 5 | lor 70 |
. 2
(a⊥ ∪ (a ∩ b)) =
(a⊥ ∪ (b⊥ ⊥ ∩
a⊥ ⊥
)) |
7 | | ancom 74 |
. . . . . 6
(a⊥ ∩ b⊥ ) = (b⊥ ∩ a⊥ ) |
8 | 2, 7 | 2or 72 |
. . . . 5
(b ∪ (a⊥ ∩ b⊥ )) = (b⊥ ⊥ ∪
(b⊥ ∩ a⊥ )) |
9 | 8 | ax-r1 35 |
. . . 4
(b⊥
⊥ ∪ (b⊥ ∩ a⊥ )) = (b ∪ (a⊥ ∩ b⊥ )) |
10 | | 2vwomr2.1 |
. . . 4
(b ∪ (a⊥ ∩ b⊥ )) = 1 |
11 | 9, 10 | ax-r2 36 |
. . 3
(b⊥
⊥ ∪ (b⊥ ∩ a⊥ )) = 1 |
12 | 11 | ax-wom 361 |
. 2
(a⊥ ∪ (b⊥ ⊥ ∩
a⊥ ⊥ )) =
1 |
13 | 6, 12 | ax-r2 36 |
1
(a⊥ ∪ (a ∩ b)) =
1 |