Proof of Theorem k1-8a
Step | Hyp | Ref
| Expression |
1 | | leo 158 |
. . 3
x ≤ (x ∪ y) |
2 | | k1-8a.2 |
. . 3
x ≤ c |
3 | 1, 2 | ler2an 173 |
. 2
x ≤ ((x ∪ y) ∩
c) |
4 | | k1-8a.3 |
. . . . 5
y ≤ c⊥ |
5 | 4 | lelor 166 |
. . . 4
(x ∪ y) ≤ (x ∪
c⊥ ) |
6 | 5 | leran 153 |
. . 3
((x ∪ y) ∩ c) ≤
((x ∪ c⊥ ) ∩ c) |
7 | | ax-a1 30 |
. . . . . 6
x = x⊥
⊥ |
8 | 7 | ror 71 |
. . . . 5
(x ∪ c⊥ ) = (x⊥ ⊥ ∪
c⊥ ) |
9 | 8 | ran 78 |
. . . 4
((x ∪ c⊥ ) ∩ c) = ((x⊥ ⊥ ∪
c⊥ ) ∩ c) |
10 | 7 | ran 78 |
. . . . . 6
(x ∩ c) = (x⊥ ⊥ ∩
c) |
11 | | k1-8a.1 |
. . . . . . 7
x⊥ = ((x⊥ ∩ c) ∪ (x⊥ ∩ c⊥ )) |
12 | 11 | k1-6 353 |
. . . . . 6
(x⊥
⊥ ∩ c) = ((x⊥ ⊥ ∪
c⊥ ) ∩ c) |
13 | 10, 12 | tr 62 |
. . . . 5
(x ∩ c) = ((x⊥ ⊥ ∪
c⊥ ) ∩ c) |
14 | 13 | cm 61 |
. . . 4
((x⊥
⊥ ∪ c⊥ ) ∩ c) = (x ∩
c) |
15 | 2 | df2le2 136 |
. . . 4
(x ∩ c) = x |
16 | 9, 14, 15 | 3tr 65 |
. . 3
((x ∪ c⊥ ) ∩ c) = x |
17 | 6, 16 | lbtr 139 |
. 2
((x ∪ y) ∩ c) ≤
x |
18 | 3, 17 | lebi 145 |
1
x = ((x ∪ y) ∩
c) |