Proof of Theorem i3or
Step | Hyp | Ref
| Expression |
1 | | le1 146 |
. 2
((a ≡ b)⊥ ∪ ((a ∪ c)
→3 (b ∪ c))) ≤ 1 |
2 | | ka4ot 435 |
. . . 4
((a ≡ b)⊥ ∪ ((a ∪ c)
≡ (b ∪ c))) = 1 |
3 | 2 | ax-r1 35 |
. . 3
1 = ((a ≡ b)⊥ ∪ ((a ∪ c)
≡ (b ∪ c))) |
4 | | i3bi 496 |
. . . . . 6
(((a ∪ c) →3 (b ∪ c))
∩ ((b ∪ c) →3 (a ∪ c))) =
((a ∪ c) ≡ (b
∪ c)) |
5 | 4 | ax-r1 35 |
. . . . 5
((a ∪ c) ≡ (b
∪ c)) = (((a ∪ c)
→3 (b ∪ c)) ∩ ((b
∪ c) →3 (a ∪ c))) |
6 | | lea 160 |
. . . . 5
(((a ∪ c) →3 (b ∪ c))
∩ ((b ∪ c) →3 (a ∪ c)))
≤ ((a ∪ c) →3 (b ∪ c)) |
7 | 5, 6 | bltr 138 |
. . . 4
((a ∪ c) ≡ (b
∪ c)) ≤ ((a ∪ c)
→3 (b ∪ c)) |
8 | 7 | lelor 166 |
. . 3
((a ≡ b)⊥ ∪ ((a ∪ c)
≡ (b ∪ c))) ≤ ((a
≡ b)⊥ ∪
((a ∪ c) →3 (b ∪ c))) |
9 | 3, 8 | bltr 138 |
. 2
1 ≤ ((a ≡ b)⊥ ∪ ((a ∪ c)
→3 (b ∪ c))) |
10 | 1, 9 | lebi 145 |
1
((a ≡ b)⊥ ∪ ((a ∪ c)
→3 (b ∪ c))) = 1 |