Proof of Theorem nomcon0
Step | Hyp | Ref
| Expression |
1 | | ax-a2 31 |
. . . 4
(a⊥ ∪ b) = (b ∪
a⊥ ) |
2 | | ax-a1 30 |
. . . . 5
b = b⊥
⊥ |
3 | 2 | ax-r5 38 |
. . . 4
(b ∪ a⊥ ) = (b⊥ ⊥ ∪
a⊥ ) |
4 | 1, 3 | ax-r2 36 |
. . 3
(a⊥ ∪ b) = (b⊥ ⊥ ∪
a⊥ ) |
5 | | ax-a2 31 |
. . . 4
(b⊥ ∪ a) = (a ∪
b⊥ ) |
6 | | ax-a1 30 |
. . . . 5
a = a⊥
⊥ |
7 | 6 | ax-r5 38 |
. . . 4
(a ∪ b⊥ ) = (a⊥ ⊥ ∪
b⊥ ) |
8 | 5, 7 | ax-r2 36 |
. . 3
(b⊥ ∪ a) = (a⊥ ⊥ ∪
b⊥ ) |
9 | 4, 8 | 2an 79 |
. 2
((a⊥ ∪ b) ∩ (b⊥ ∪ a)) = ((b⊥ ⊥ ∪
a⊥ ) ∩ (a⊥ ⊥ ∪
b⊥ )) |
10 | | df-id0 49 |
. 2
(a ≡0 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ a)) |
11 | | df-id0 49 |
. 2
(b⊥ ≡0
a⊥ ) = ((b⊥ ⊥ ∪
a⊥ ) ∩ (a⊥ ⊥ ∪
b⊥ )) |
12 | 9, 10, 11 | 3tr1 63 |
1
(a ≡0 b) = (b⊥ ≡0 a⊥ ) |