Proof of Theorem i3orlem6
Step | Hyp | Ref
| Expression |
1 | | ax-a3 32 |
. . 3
(((a ∩ b) ∪ (a
→3 b)⊥ )
∪ ((a ∪ c) →3 (b ∪ c))) =
((a ∩ b) ∪ ((a
→3 b)⊥
∪ ((a ∪ c) →3 (b ∪ c)))) |
2 | 1 | ax-r1 35 |
. 2
((a ∩ b) ∪ ((a
→3 b)⊥
∪ ((a ∪ c) →3 (b ∪ c)))) =
(((a ∩ b) ∪ (a
→3 b)⊥ )
∪ ((a ∪ c) →3 (b ∪ c))) |
3 | | i3orlem2 553 |
. . . 4
(a ∩ b) ≤ ((a
∪ c) →3 (b ∪ c)) |
4 | 3 | lerr 150 |
. . 3
(a ∩ b) ≤ ((a
→3 b)⊥
∪ ((a ∪ c) →3 (b ∪ c))) |
5 | 4 | df-le2 131 |
. 2
((a ∩ b) ∪ ((a
→3 b)⊥
∪ ((a ∪ c) →3 (b ∪ c)))) =
((a →3 b)⊥ ∪ ((a ∪ c)
→3 (b ∪ c))) |
6 | | oi3ai3 503 |
. . 3
((a ∩ b) ∪ (a
→3 b)⊥ ) =
((a ∪ b) ∩ (a⊥ →3 b⊥ )) |
7 | 6 | ax-r5 38 |
. 2
(((a ∩ b) ∪ (a
→3 b)⊥ )
∪ ((a ∪ c) →3 (b ∪ c))) =
(((a ∪ b) ∩ (a⊥ →3 b⊥ )) ∪ ((a ∪ c)
→3 (b ∪ c))) |
8 | 2, 5, 7 | 3tr2 64 |
1
((a →3 b)⊥ ∪ ((a ∪ c)
→3 (b ∪ c))) = (((a
∪ b) ∩ (a⊥ →3 b⊥ )) ∪ ((a ∪ c)
→3 (b ∪ c))) |