Proof of Theorem wom2
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | le1 146 |
. 2
a ≤ 1 |
| 2 | | conb 122 |
. . . . . 6
(a ≡ b) = (a⊥ ≡ b⊥ ) |
| 3 | 2 | ax-r4 37 |
. . . . 5
(a ≡ b)⊥ = (a⊥ ≡ b⊥
)⊥ |
| 4 | | oran 87 |
. . . . . . 7
(a ∪ c) = (a⊥ ∩ c⊥
)⊥ |
| 5 | | oran 87 |
. . . . . . 7
(b ∪ c) = (b⊥ ∩ c⊥
)⊥ |
| 6 | 4, 5 | 2bi 99 |
. . . . . 6
((a ∪ c) ≡ (b
∪ c)) = ((a⊥ ∩ c⊥ )⊥ ≡
(b⊥ ∩ c⊥ )⊥
) |
| 7 | | conb 122 |
. . . . . . 7
((a⊥ ∩ c⊥ ) ≡ (b⊥ ∩ c⊥ )) = ((a⊥ ∩ c⊥ )⊥ ≡
(b⊥ ∩ c⊥ )⊥
) |
| 8 | 7 | ax-r1 35 |
. . . . . 6
((a⊥ ∩ c⊥ )⊥ ≡
(b⊥ ∩ c⊥ )⊥ ) =
((a⊥ ∩ c⊥ ) ≡ (b⊥ ∩ c⊥ )) |
| 9 | 6, 8 | ax-r2 36 |
. . . . 5
((a ∪ c) ≡ (b
∪ c)) = ((a⊥ ∩ c⊥ ) ≡ (b⊥ ∩ c⊥ )) |
| 10 | 3, 9 | 2or 72 |
. . . 4
((a ≡ b)⊥ ∪ ((a ∪ c)
≡ (b ∪ c))) = ((a⊥ ≡ b⊥ )⊥ ∪
((a⊥ ∩ c⊥ ) ≡ (b⊥ ∩ c⊥ ))) |
| 11 | | ska4 433 |
. . . 4
((a⊥ ≡
b⊥ )⊥
∪ ((a⊥ ∩ c⊥ ) ≡ (b⊥ ∩ c⊥ ))) = 1 |
| 12 | 10, 11 | ax-r2 36 |
. . 3
((a ≡ b)⊥ ∪ ((a ∪ c)
≡ (b ∪ c))) = 1 |
| 13 | 12 | ax-r1 35 |
. 2
1 = ((a ≡ b)⊥ ∪ ((a ∪ c)
≡ (b ∪ c))) |
| 14 | 1, 13 | lbtr 139 |
1
a ≤ ((a ≡ b)⊥ ∪ ((a ∪ c)
≡ (b ∪ c))) |
