Proof of Theorem axoa4
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | u1lem9b 778 |
. . 3
a⊥ ≤ (a →1 d) |
| 2 | 1 | leran 153 |
. 2
(a⊥ ∩ (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
∪ (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)))))))) |
| 3 | | ax-4oa 1033 |
. . . 4
(((b →1 d) →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)))))) ≤ ((a
→1 d) →1
d) |
| 4 | | id 59 |
. . . 4
(a →1 d) = (a
→1 d) |
| 5 | | id 59 |
. . . 4
(b →1 d) = (b
→1 d) |
| 6 | | id 59 |
. . . 4
(c →1 d) = (c
→1 d) |
| 7 | 3, 4, 5, 6 | oa4gto4u 976 |
. . 3
((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 |
| 8 | 7 | oa4uto4 977 |
. 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)))))))) ≤ d |
| 9 | 2, 8 | letr 137 |
1
(a⊥ ∩ (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 |
