Proof of Theorem oa4uto4
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | u1lem9a 777 |
. . . . 5
(a⊥ →1
d)⊥ ≤ a⊥ |
| 2 | 1 | lecon1 155 |
. . . 4
a ≤ (a⊥ →1 d) |
| 3 | | u1lem9a 777 |
. . . . . 6
(b⊥ →1
d)⊥ ≤ b⊥ |
| 4 | 3 | lecon1 155 |
. . . . 5
b ≤ (b⊥ →1 d) |
| 5 | | ax-a2 31 |
. . . . . . 7
((a ∩ b) ∪ ((a
→1 d) ∩ (b →1 d))) = (((a
→1 d) ∩ (b →1 d)) ∪ (a
∩ b)) |
| 6 | 2, 4 | le2an 169 |
. . . . . . . 8
(a ∩ b) ≤ ((a⊥ →1 d) ∩ (b⊥ →1 d)) |
| 7 | 6 | lelor 166 |
. . . . . . 7
(((a →1 d) ∩ (b
→1 d)) ∪ (a ∩ b)) ≤
(((a →1 d) ∩ (b
→1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) |
| 8 | 5, 7 | bltr 138 |
. . . . . 6
((a ∩ b) ∪ ((a
→1 d) ∩ (b →1 d))) ≤ (((a
→1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) |
| 9 | | ax-a2 31 |
. . . . . . . 8
((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) = (((a
→1 d) ∩ (c →1 d)) ∪ (a
∩ c)) |
| 10 | | u1lem9a 777 |
. . . . . . . . . . 11
(c⊥ →1
d)⊥ ≤ c⊥ |
| 11 | 10 | lecon1 155 |
. . . . . . . . . 10
c ≤ (c⊥ →1 d) |
| 12 | 2, 11 | le2an 169 |
. . . . . . . . 9
(a ∩ c) ≤ ((a⊥ →1 d) ∩ (c⊥ →1 d)) |
| 13 | 12 | lelor 166 |
. . . . . . . 8
(((a →1 d) ∩ (c
→1 d)) ∪ (a ∩ c)) ≤
(((a →1 d) ∩ (c
→1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) |
| 14 | 9, 13 | bltr 138 |
. . . . . . 7
((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ≤ (((a
→1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) |
| 15 | | ax-a2 31 |
. . . . . . . 8
((b ∩ c) ∪ ((b
→1 d) ∩ (c →1 d))) = (((b
→1 d) ∩ (c →1 d)) ∪ (b
∩ c)) |
| 16 | 4, 11 | le2an 169 |
. . . . . . . . 9
(b ∩ c) ≤ ((b⊥ →1 d) ∩ (c⊥ →1 d)) |
| 17 | 16 | lelor 166 |
. . . . . . . 8
(((b →1 d) ∩ (c
→1 d)) ∪ (b ∩ c)) ≤
(((b →1 d) ∩ (c
→1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d))) |
| 18 | 15, 17 | bltr 138 |
. . . . . . 7
((b ∩ c) ∪ ((b
→1 d) ∩ (c →1 d))) ≤ (((b
→1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d))) |
| 19 | 14, 18 | le2an 169 |
. . . . . 6
(((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d)))) ≤ ((((a →1 d) ∩ (c
→1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b
→1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))) |
| 20 | 8, 19 | le2or 168 |
. . . . 5
(((a ∩ b) ∪ ((a
→1 d) ∩ (b →1 d))) ∪ (((a
∩ c) ∪ ((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c) ∪
((b →1 d) ∩ (c
→1 d))))) ≤ ((((a →1 d) ∩ (b
→1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a
→1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b
→1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d))))) |
| 21 | 4, 20 | le2an 169 |
. . . 4
(b ∩ (((a ∩ b) ∪
((a →1 d) ∩ (b
→1 d))) ∪ (((a ∩ c) ∪
((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c) ∪
((b →1 d) ∩ (c
→1 d)))))) ≤ ((b⊥ →1 d) ∩ ((((a
→1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a
→1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b
→1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))) |
| 22 | 2, 21 | le2or 168 |
. . 3
(a ∪ (b ∩ (((a
∩ b) ∪ ((a →1 d) ∩ (b
→1 d))) ∪ (((a ∩ c) ∪
((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c) ∪
((b →1 d) ∩ (c
→1 d))))))) ≤ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a
→1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a
→1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b
→1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d))))))) |
| 23 | 22 | lelan 167 |
. 2
((a →1 d) ∩ (a
∪ (b ∩ (((a ∩ b) ∪
((a →1 d) ∩ (b
→1 d))) ∪ (((a ∩ c) ∪
((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c) ∪
((b →1 d) ∩ (c
→1 d)))))))) ≤
((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a
→1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a
→1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b
→1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) |
| 24 | | oa4uto4.1 |
. 2
((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a
→1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a
→1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b
→1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) ≤ d |
| 25 | 23, 24 | letr 137 |
1
((a →1 d) ∩ (a
∪ (b ∩ (((a ∩ b) ∪
((a →1 d) ∩ (b
→1 d))) ∪ (((a ∩ c) ∪
((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c) ∪
((b →1 d) ∩ (c
→1 d)))))))) ≤ d |
