Proof of Theorem oa8to5
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | oa8to5.1 |
. . 3
(((a⊥ ∪
b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ ))) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))))))) |
| 2 | 1 | oa8todual 971 |
. 2
(b ∩ (a ∪ (c ∩
((((a ∩ c) ∪ (b
∩ d)) ∪ (((a ∩ g) ∪
(b ∩ h)) ∩ ((c
∩ g) ∪ (d ∩ h))))
∪ ((((a ∩ e) ∪ (b
∩ f)) ∪ (((a ∩ g) ∪
(b ∩ h)) ∩ ((e
∩ g) ∪ (f ∩ h))))
∩ (((c ∩ e) ∪ (d
∩ f)) ∪ (((c ∩ g) ∪
(d ∩ h)) ∩ ((e
∩ g) ∪ (f ∩ h))))))))) ≤ (((a ∩ b) ∪
(c ∩ d)) ∪ ((e
∩ f) ∪ (g ∩ h))) |
| 3 | | oa8to5.2 |
. . . 4
b⊥ = (a →1 j)⊥ |
| 4 | 3 | con1 66 |
. . 3
b = (a →1 j) |
| 5 | | oa8to5.3 |
. . . . . . . . . 10
d⊥ = (c →1 j)⊥ |
| 6 | 5 | con1 66 |
. . . . . . . . 9
d = (c →1 j) |
| 7 | 4, 6 | 2an 79 |
. . . . . . . 8
(b ∩ d) = ((a
→1 j) ∩ (c →1 j)) |
| 8 | 7 | lor 70 |
. . . . . . 7
((a ∩ c) ∪ (b
∩ d)) = ((a ∩ c) ∪
((a →1 j) ∩ (c
→1 j))) |
| 9 | | oa8to5.5 |
. . . . . . . . . . 11
h⊥ = (g →1 j)⊥ |
| 10 | 9 | con1 66 |
. . . . . . . . . 10
h = (g →1 j) |
| 11 | 4, 10 | 2an 79 |
. . . . . . . . 9
(b ∩ h) = ((a
→1 j) ∩ (g →1 j)) |
| 12 | 11 | lor 70 |
. . . . . . . 8
((a ∩ g) ∪ (b
∩ h)) = ((a ∩ g) ∪
((a →1 j) ∩ (g
→1 j))) |
| 13 | 6, 10 | 2an 79 |
. . . . . . . . 9
(d ∩ h) = ((c
→1 j) ∩ (g →1 j)) |
| 14 | 13 | lor 70 |
. . . . . . . 8
((c ∩ g) ∪ (d
∩ h)) = ((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))) |
| 15 | 12, 14 | 2an 79 |
. . . . . . 7
(((a ∩ g) ∪ (b
∩ h)) ∩ ((c ∩ g) ∪
(d ∩ h))) = (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j)))) |
| 16 | 8, 15 | 2or 72 |
. . . . . 6
(((a ∩ c) ∪ (b
∩ d)) ∪ (((a ∩ g) ∪
(b ∩ h)) ∩ ((c
∩ g) ∪ (d ∩ h)))) =
(((a ∩ c) ∪ ((a
→1 j) ∩ (c →1 j))) ∪ (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))))) |
| 17 | | oa8to5.4 |
. . . . . . . . . . 11
f⊥ = (e →1 j)⊥ |
| 18 | 17 | con1 66 |
. . . . . . . . . 10
f = (e →1 j) |
| 19 | 4, 18 | 2an 79 |
. . . . . . . . 9
(b ∩ f) = ((a
→1 j) ∩ (e →1 j)) |
| 20 | 19 | lor 70 |
. . . . . . . 8
((a ∩ e) ∪ (b
∩ f)) = ((a ∩ e) ∪
((a →1 j) ∩ (e
→1 j))) |
| 21 | 18, 10 | 2an 79 |
. . . . . . . . . 10
(f ∩ h) = ((e
→1 j) ∩ (g →1 j)) |
| 22 | 21 | lor 70 |
. . . . . . . . 9
((e ∩ g) ∪ (f
∩ h)) = ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j))) |
| 23 | 12, 22 | 2an 79 |
. . . . . . . 8
(((a ∩ g) ∪ (b
∩ h)) ∩ ((e ∩ g) ∪
(f ∩ h))) = (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j)))) |
| 24 | 20, 23 | 2or 72 |
. . . . . . 7
(((a ∩ e) ∪ (b
∩ f)) ∪ (((a ∩ g) ∪
(b ∩ h)) ∩ ((e
∩ g) ∪ (f ∩ h)))) =
(((a ∩ e) ∪ ((a
→1 j) ∩ (e →1 j))) ∪ (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j))))) |
| 25 | 6, 18 | 2an 79 |
. . . . . . . . 9
(d ∩ f) = ((c
→1 j) ∩ (e →1 j)) |
| 26 | 25 | lor 70 |
. . . . . . . 8
((c ∩ e) ∪ (d
∩ f)) = ((c ∩ e) ∪
((c →1 j) ∩ (e
→1 j))) |
| 27 | 14, 22 | 2an 79 |
. . . . . . . 8
(((c ∩ g) ∪ (d
∩ h)) ∩ ((e ∩ g) ∪
(f ∩ h))) = (((c
∩ g) ∪ ((c →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j)))) |
| 28 | 26, 27 | 2or 72 |
. . . . . . 7
(((c ∩ e) ∪ (d
∩ f)) ∪ (((c ∩ g) ∪
(d ∩ h)) ∩ ((e
∩ g) ∪ (f ∩ h)))) =
(((c ∩ e) ∪ ((c
→1 j) ∩ (e →1 j))) ∪ (((c
∩ g) ∪ ((c →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j))))) |
| 29 | 24, 28 | 2an 79 |
. . . . . 6
((((a ∩ e) ∪ (b
∩ f)) ∪ (((a ∩ g) ∪
(b ∩ h)) ∩ ((e
∩ g) ∪ (f ∩ h))))
∩ (((c ∩ e) ∪ (d
∩ f)) ∪ (((c ∩ g) ∪
(d ∩ h)) ∩ ((e
∩ g) ∪ (f ∩ h))))) =
((((a ∩ e) ∪ ((a
→1 j) ∩ (e →1 j))) ∪ (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j))))) ∩ (((c ∩ e) ∪
((c →1 j) ∩ (e
→1 j))) ∪ (((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j)))))) |
| 30 | 16, 29 | 2or 72 |
. . . . 5
((((a ∩ c) ∪ (b
∩ d)) ∪ (((a ∩ g) ∪
(b ∩ h)) ∩ ((c
∩ g) ∪ (d ∩ h))))
∪ ((((a ∩ e) ∪ (b
∩ f)) ∪ (((a ∩ g) ∪
(b ∩ h)) ∩ ((e
∩ g) ∪ (f ∩ h))))
∩ (((c ∩ e) ∪ (d
∩ f)) ∪ (((c ∩ g) ∪
(d ∩ h)) ∩ ((e
∩ g) ∪ (f ∩ h))))))
= ((((a ∩ c) ∪ ((a
→1 j) ∩ (c →1 j))) ∪ (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))))) ∪
((((a ∩ e) ∪ ((a
→1 j) ∩ (e →1 j))) ∪ (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j))))) ∩ (((c ∩ e) ∪
((c →1 j) ∩ (e
→1 j))) ∪ (((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j))))))) |
| 31 | 30 | lan 77 |
. . . 4
(c ∩ ((((a ∩ c) ∪
(b ∩ d)) ∪ (((a
∩ g) ∪ (b ∩ h))
∩ ((c ∩ g) ∪ (d
∩ h)))) ∪ ((((a ∩ e) ∪
(b ∩ f)) ∪ (((a
∩ g) ∪ (b ∩ h))
∩ ((e ∩ g) ∪ (f
∩ h)))) ∩ (((c ∩ e) ∪
(d ∩ f)) ∪ (((c
∩ g) ∪ (d ∩ h))
∩ ((e ∩ g) ∪ (f
∩ h))))))) = (c ∩ ((((a
∩ c) ∪ ((a →1 j) ∩ (c
→1 j))) ∪ (((a ∩ g) ∪
((a →1 j) ∩ (g
→1 j))) ∩ ((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))))) ∪
((((a ∩ e) ∪ ((a
→1 j) ∩ (e →1 j))) ∪ (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j))))) ∩ (((c ∩ e) ∪
((c →1 j) ∩ (e
→1 j))) ∪ (((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j)))))))) |
| 32 | 31 | lor 70 |
. . 3
(a ∪ (c ∩ ((((a
∩ c) ∪ (b ∩ d))
∪ (((a ∩ g) ∪ (b
∩ h)) ∩ ((c ∩ g) ∪
(d ∩ h)))) ∪ ((((a ∩ e) ∪
(b ∩ f)) ∪ (((a
∩ g) ∪ (b ∩ h))
∩ ((e ∩ g) ∪ (f
∩ h)))) ∩ (((c ∩ e) ∪
(d ∩ f)) ∪ (((c
∩ g) ∪ (d ∩ h))
∩ ((e ∩ g) ∪ (f
∩ h)))))))) = (a ∪ (c ∩
((((a ∩ c) ∪ ((a
→1 j) ∩ (c →1 j))) ∪ (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))))) ∪
((((a ∩ e) ∪ ((a
→1 j) ∩ (e →1 j))) ∪ (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j))))) ∩ (((c ∩ e) ∪
((c →1 j) ∩ (e
→1 j))) ∪ (((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j))))))))) |
| 33 | 4, 32 | 2an 79 |
. 2
(b ∩ (a ∪ (c ∩
((((a ∩ c) ∪ (b
∩ d)) ∪ (((a ∩ g) ∪
(b ∩ h)) ∩ ((c
∩ g) ∪ (d ∩ h))))
∪ ((((a ∩ e) ∪ (b
∩ f)) ∪ (((a ∩ g) ∪
(b ∩ h)) ∩ ((e
∩ g) ∪ (f ∩ h))))
∩ (((c ∩ e) ∪ (d
∩ f)) ∪ (((c ∩ g) ∪
(d ∩ h)) ∩ ((e
∩ g) ∪ (f ∩ h))))))))) = ((a
→1 j) ∩ (a ∪ (c ∩
((((a ∩ c) ∪ ((a
→1 j) ∩ (c →1 j))) ∪ (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))))) ∪
((((a ∩ e) ∪ ((a
→1 j) ∩ (e →1 j))) ∪ (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j))))) ∩ (((c ∩ e) ∪
((c →1 j) ∩ (e
→1 j))) ∪ (((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j)))))))))) |
| 34 | 4 | lan 77 |
. . . . 5
(a ∩ b) = (a ∩
(a →1 j)) |
| 35 | | ancom 74 |
. . . . 5
(a ∩ (a →1 j)) = ((a
→1 j) ∩ a) |
| 36 | | u1lemaa 600 |
. . . . 5
((a →1 j) ∩ a) =
(a ∩ j) |
| 37 | 34, 35, 36 | 3tr 65 |
. . . 4
(a ∩ b) = (a ∩
j) |
| 38 | 6 | lan 77 |
. . . . 5
(c ∩ d) = (c ∩
(c →1 j)) |
| 39 | | ancom 74 |
. . . . 5
(c ∩ (c →1 j)) = ((c
→1 j) ∩ c) |
| 40 | | u1lemaa 600 |
. . . . 5
((c →1 j) ∩ c) =
(c ∩ j) |
| 41 | 38, 39, 40 | 3tr 65 |
. . . 4
(c ∩ d) = (c ∩
j) |
| 42 | 37, 41 | 2or 72 |
. . 3
((a ∩ b) ∪ (c
∩ d)) = ((a ∩ j) ∪
(c ∩ j)) |
| 43 | 18 | lan 77 |
. . . . 5
(e ∩ f) = (e ∩
(e →1 j)) |
| 44 | | ancom 74 |
. . . . 5
(e ∩ (e →1 j)) = ((e
→1 j) ∩ e) |
| 45 | | u1lemaa 600 |
. . . . 5
((e →1 j) ∩ e) =
(e ∩ j) |
| 46 | 43, 44, 45 | 3tr 65 |
. . . 4
(e ∩ f) = (e ∩
j) |
| 47 | 10 | lan 77 |
. . . . 5
(g ∩ h) = (g ∩
(g →1 j)) |
| 48 | | ancom 74 |
. . . . 5
(g ∩ (g →1 j)) = ((g
→1 j) ∩ g) |
| 49 | | u1lemaa 600 |
. . . . 5
((g →1 j) ∩ g) =
(g ∩ j) |
| 50 | 47, 48, 49 | 3tr 65 |
. . . 4
(g ∩ h) = (g ∩
j) |
| 51 | 46, 50 | 2or 72 |
. . 3
((e ∩ f) ∪ (g
∩ h)) = ((e ∩ j) ∪
(g ∩ j)) |
| 52 | 42, 51 | 2or 72 |
. 2
(((a ∩ b) ∪ (c
∩ d)) ∪ ((e ∩ f) ∪
(g ∩ h))) = (((a
∩ j) ∪ (c ∩ j))
∪ ((e ∩ j) ∪ (g
∩ j))) |
| 53 | 2, 33, 52 | le3tr2 141 |
1
((a →1 j) ∩ (a
∪ (c ∩ ((((a ∩ c) ∪
((a →1 j) ∩ (c
→1 j))) ∪ (((a ∩ g) ∪
((a →1 j) ∩ (g
→1 j))) ∩ ((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))))) ∪
((((a ∩ e) ∪ ((a
→1 j) ∩ (e →1 j))) ∪ (((a
∩ g) ∪ ((a →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j))))) ∩ (((c ∩ e) ∪
((c →1 j) ∩ (e
→1 j))) ∪ (((c ∩ g) ∪
((c →1 j) ∩ (g
→1 j))) ∩ ((e ∩ g) ∪
((e →1 j) ∩ (g
→1 j)))))))))) ≤
(((a ∩ j) ∪ (c
∩ j)) ∪ ((e ∩ j) ∪
(g ∩ j))) |
