Proof of Theorem lem3.3.5
Step | Hyp | Ref
| Expression |
1 | | df-b1 1048 |
. . . . . 6
(a ↔1 b) = ((a
→1 b) ∩ (b →1 a)) |
2 | | lea 160 |
. . . . . 6
((a →1 b) ∩ (b
→1 a)) ≤ (a →1 b) |
3 | 1, 2 | bltr 138 |
. . . . 5
(a ↔1 b) ≤ (a
→1 b) |
4 | | df-i1 44 |
. . . . 5
(a →1 b) = (a⊥ ∪ (a ∩ b)) |
5 | 3, 4 | lbtr 139 |
. . . 4
(a ↔1 b) ≤ (a⊥ ∪ (a ∩ b)) |
6 | | leo 158 |
. . . . . 6
b ≤ (b ∪ c) |
7 | 6 | lelan 167 |
. . . . 5
(a ∩ b) ≤ (a ∩
(b ∪ c)) |
8 | 7 | lelor 166 |
. . . 4
(a⊥ ∪ (a ∩ b)) ≤
(a⊥ ∪ (a ∩ (b ∪
c))) |
9 | 5, 8 | letr 137 |
. . 3
(a ↔1 b) ≤ (a⊥ ∪ (a ∩ (b ∪
c))) |
10 | | lem3.3.5.1 |
. . . . 5
(a ≡5 b) = 1 |
11 | | lem3.3.3 1052 |
. . . . 5
((a ≡5 b) →0 (a ↔1 b)) = 1 |
12 | 10, 11 | lem3.3.2 1046 |
. . . 4
(a ↔1 b) = 1 |
13 | 12 | ax-r1 35 |
. . 3
1 = (a ↔1 b) |
14 | | df-i1 44 |
. . 3
(a →1 (b ∪ c)) =
(a⊥ ∪ (a ∩ (b ∪
c))) |
15 | 9, 13, 14 | le3tr1 140 |
. 2
1 ≤ (a →1
(b ∪ c)) |
16 | 15 | lem3.3.5lem 1054 |
1
(a →1 (b ∪ c)) =
1 |