Proof of Theorem oa6
Step | Hyp | Ref
| Expression |
1 | | oa6.1 |
. 2
a ≤ b⊥ |
2 | | oa6.2 |
. 2
c ≤ d⊥ |
3 | | oa6.3 |
. 2
e ≤ f⊥ |
4 | | id 59 |
. 2
(((a⊥ ∩
b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )) = (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )) |
5 | | id 59 |
. 2
a⊥ = a⊥ |
6 | | id 59 |
. 2
c⊥ = c⊥ |
7 | | id 59 |
. 2
e⊥ = e⊥ |
8 | | axoa4b 1035 |
. 2
((a⊥ →1
(((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∪ (((a⊥ ∩ e⊥ ) ∪ ((a⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))))) ∩ ((c⊥ ∩ e⊥ ) ∪ ((c⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))) ∩ (e⊥ →1 (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )))))))))) ≤ (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ )) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | oa4to6 965 |
1
(((a ∪ b) ∩ (c
∪ d)) ∩ (e ∪ f)) ≤
(b ∪ (a ∩ (c ∪
(((a ∪ c) ∩ (b
∪ d)) ∩ (((a ∪ e) ∩
(b ∪ f)) ∪ ((c
∪ e) ∩ (d ∪ f))))))) |