Proof of Theorem 4oa
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | 4oa.2 |
. . 3
f = (((a ∩ b) ∪
((a →1 d) ∩ (b
→1 d))) ∪ e) |
| 2 | 1 | lan 77 |
. 2
((a →1 d) ∩ f) =
((a →1 d) ∩ (((a
∩ b) ∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)) |
| 3 | | axoa4a 1037 |
. . . 4
(((b⊥
⊥ →1 d)
→1 d) ∩ ((b⊥ ⊥ →1
d) ∪ ((a⊥ ⊥ →1
d) ∩ ((((b⊥ ⊥ →1
d) ∩ (a⊥ ⊥ →1
d)) ∪ (((b⊥ ⊥ →1
d) →1 d) ∩ ((a⊥ ⊥ →1
d) →1 d))) ∪ ((((b⊥ ⊥ →1
d) ∩ (c⊥ ⊥ →1
d)) ∪ (((b⊥ ⊥ →1
d) →1 d) ∩ ((c⊥ ⊥ →1
d) →1 d))) ∩ (((a⊥ ⊥ →1
d) ∩ (c⊥ ⊥ →1
d)) ∪ (((a⊥ ⊥ →1
d) →1 d) ∩ ((c⊥ ⊥ →1
d) →1 d)))))))) ≤ ((((b⊥ ⊥ →1
d) ∩ d) ∪ ((a⊥ ⊥ →1
d) ∩ d)) ∪ ((c⊥ ⊥ →1
d) ∩ d)) |
| 4 | | id 59 |
. . . 4
(b⊥
⊥ →1 d) =
(b⊥ ⊥
→1 d) |
| 5 | | id 59 |
. . . 4
(a⊥
⊥ →1 d) =
(a⊥ ⊥
→1 d) |
| 6 | | id 59 |
. . . 4
(c⊥
⊥ →1 d) =
(c⊥ ⊥
→1 d) |
| 7 | 3, 4, 5, 6 | oa4to4u2 974 |
. . 3
((b⊥ →1
d) ∩ ((b⊥ ⊥ →1
d) ∪ ((a⊥ ⊥ →1
d) ∩ ((((b⊥ →1 d) ∩ (a⊥ →1 d)) ∪ ((b⊥ ⊥ →1
d) ∩ (a⊥ ⊥ →1
d))) ∪ ((((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((b⊥ ⊥ →1
d) ∩ (c⊥ ⊥ →1
d))) ∩ (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ ((a⊥ ⊥ →1
d) ∩ (c⊥ ⊥ →1
d)))))))) ≤ d |
| 8 | | 4oa.1 |
. . 3
e = (((a ∩ c) ∪
((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c) ∪
((b →1 d) ∩ (c
→1 d)))) |
| 9 | 7, 8 | oa4uto4g 975 |
. 2
((a →1 d) ∩ (((a
∩ b) ∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)) ≤ (b
→1 d) |
| 10 | 2, 9 | bltr 138 |
1
((a →1 d) ∩ f) ≤
(b →1 d) |
