Proof of Theorem oat
Step | Hyp | Ref
| Expression |
1 | | leor 159 |
. . 3
b ≤ (a ∪ b) |
2 | | oml 445 |
. . . . 5
(a ∪ (a⊥ ∩ (a ∪ b))) =
(a ∪ b) |
3 | 2 | ax-r1 35 |
. . . 4
(a ∪ b) = (a ∪
(a⊥ ∩ (a ∪ b))) |
4 | | lea 160 |
. . . . . 6
(a⊥ ∩ (a ∪ b)) ≤
a⊥ |
5 | | oat.1 |
. . . . . 6
(a⊥ ∩ (a ∪ b)) ≤
c |
6 | 4, 5 | ler2an 173 |
. . . . 5
(a⊥ ∩ (a ∪ b)) ≤
(a⊥ ∩ c) |
7 | 6 | lelor 166 |
. . . 4
(a ∪ (a⊥ ∩ (a ∪ b)))
≤ (a ∪ (a⊥ ∩ c)) |
8 | 3, 7 | bltr 138 |
. . 3
(a ∪ b) ≤ (a ∪
(a⊥ ∩ c)) |
9 | 1, 8 | letr 137 |
. 2
b ≤ (a ∪ (a⊥ ∩ c)) |
10 | | ax-a1 30 |
. . . 4
a = a⊥
⊥ |
11 | 10 | ax-r5 38 |
. . 3
(a ∪ (a⊥ ∩ c)) = (a⊥ ⊥ ∪
(a⊥ ∩ c)) |
12 | | df-i1 44 |
. . . 4
(a⊥ →1
c) = (a⊥ ⊥ ∪
(a⊥ ∩ c)) |
13 | 12 | ax-r1 35 |
. . 3
(a⊥
⊥ ∪ (a⊥ ∩ c)) = (a⊥ →1 c) |
14 | 11, 13 | ax-r2 36 |
. 2
(a ∪ (a⊥ ∩ c)) = (a⊥ →1 c) |
15 | 9, 14 | lbtr 139 |
1
b ≤ (a⊥ →1 c) |