Proof of Theorem oatr
Step | Hyp | Ref
| Expression |
1 | | leo 158 |
. . . . 5
a ≤ (a ∪ (a⊥ ∩ c)) |
2 | | oatr.1 |
. . . . . 6
b ≤ (a⊥ →1 c) |
3 | | df-i1 44 |
. . . . . . 7
(a⊥ →1
c) = (a⊥ ⊥ ∪
(a⊥ ∩ c)) |
4 | | ax-a1 30 |
. . . . . . . . 9
a = a⊥
⊥ |
5 | 4 | ax-r5 38 |
. . . . . . . 8
(a ∪ (a⊥ ∩ c)) = (a⊥ ⊥ ∪
(a⊥ ∩ c)) |
6 | 5 | ax-r1 35 |
. . . . . . 7
(a⊥
⊥ ∪ (a⊥ ∩ c)) = (a ∪
(a⊥ ∩ c)) |
7 | 3, 6 | ax-r2 36 |
. . . . . 6
(a⊥ →1
c) = (a ∪ (a⊥ ∩ c)) |
8 | 2, 7 | lbtr 139 |
. . . . 5
b ≤ (a ∪ (a⊥ ∩ c)) |
9 | 1, 8 | lel2or 170 |
. . . 4
(a ∪ b) ≤ (a ∪
(a⊥ ∩ c)) |
10 | 9 | lelan 167 |
. . 3
(a⊥ ∩ (a ∪ b)) ≤
(a⊥ ∩ (a ∪ (a⊥ ∩ c))) |
11 | | omlan 448 |
. . 3
(a⊥ ∩ (a ∪ (a⊥ ∩ c))) = (a⊥ ∩ c) |
12 | 10, 11 | lbtr 139 |
. 2
(a⊥ ∩ (a ∪ b)) ≤
(a⊥ ∩ c) |
13 | | lear 161 |
. 2
(a⊥ ∩ c) ≤ c |
14 | 12, 13 | letr 137 |
1
(a⊥ ∩ (a ∪ b)) ≤
c |