Proof of Theorem ska15
Step | Hyp | Ref
| Expression |
1 | | df-i3 46 |
. . 3
(a →3 b) = (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))) |
2 | | ax-a2 31 |
. . . . . 6
((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)) |
3 | | lea 160 |
. . . . . . 7
(a⊥ ∩ b⊥ ) ≤ a⊥ |
4 | | lear 161 |
. . . . . . 7
(a⊥ ∩ b) ≤ b |
5 | 3, 4 | le2or 168 |
. . . . . 6
((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)) ≤ (a⊥ ∪ b) |
6 | 2, 5 | bltr 138 |
. . . . 5
((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ≤ (a⊥ ∪ b) |
7 | | lear 161 |
. . . . 5
(a ∩ (a⊥ ∪ b)) ≤ (a⊥ ∪ b) |
8 | 6, 7 | le2or 168 |
. . . 4
(((a⊥ ∩
b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))) ≤ ((a⊥ ∪ b) ∪ (a⊥ ∪ b)) |
9 | | oridm 110 |
. . . 4
((a⊥ ∪ b) ∪ (a⊥ ∪ b)) = (a⊥ ∪ b) |
10 | 8, 9 | lbtr 139 |
. . 3
(((a⊥ ∩
b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))) ≤ (a⊥ ∪ b) |
11 | 1, 10 | bltr 138 |
. 2
(a →3 b) ≤ (a⊥ ∪ b) |
12 | 11 | sklem 230 |
1
((a →3 b)⊥ ∪ (a⊥ ∪ b)) = 1 |