Proof of Theorem cvnbtwn4
Step | Hyp | Ref
| Expression |
1 | | cvnbtwn 30656 |
. 2
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ (𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵))) |
2 | | iman 402 |
. . 3
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) → (𝐶 = 𝐴 ∨ 𝐶 = 𝐵)) ↔ ¬ ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) ∧ ¬ (𝐶 = 𝐴 ∨ 𝐶 = 𝐵))) |
3 | | an4 653 |
. . . . 5
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) ∧ (¬ 𝐴 = 𝐶 ∧ ¬ 𝐶 = 𝐵)) ↔ ((𝐴 ⊆ 𝐶 ∧ ¬ 𝐴 = 𝐶) ∧ (𝐶 ⊆ 𝐵 ∧ ¬ 𝐶 = 𝐵))) |
4 | | ioran 981 |
. . . . . . 7
⊢ (¬
(𝐶 = 𝐴 ∨ 𝐶 = 𝐵) ↔ (¬ 𝐶 = 𝐴 ∧ ¬ 𝐶 = 𝐵)) |
5 | | eqcom 2745 |
. . . . . . . . 9
⊢ (𝐶 = 𝐴 ↔ 𝐴 = 𝐶) |
6 | 5 | notbii 320 |
. . . . . . . 8
⊢ (¬
𝐶 = 𝐴 ↔ ¬ 𝐴 = 𝐶) |
7 | 6 | anbi1i 624 |
. . . . . . 7
⊢ ((¬
𝐶 = 𝐴 ∧ ¬ 𝐶 = 𝐵) ↔ (¬ 𝐴 = 𝐶 ∧ ¬ 𝐶 = 𝐵)) |
8 | 4, 7 | bitri 274 |
. . . . . 6
⊢ (¬
(𝐶 = 𝐴 ∨ 𝐶 = 𝐵) ↔ (¬ 𝐴 = 𝐶 ∧ ¬ 𝐶 = 𝐵)) |
9 | 8 | anbi2i 623 |
. . . . 5
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) ∧ ¬ (𝐶 = 𝐴 ∨ 𝐶 = 𝐵)) ↔ ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) ∧ (¬ 𝐴 = 𝐶 ∧ ¬ 𝐶 = 𝐵))) |
10 | | dfpss2 4019 |
. . . . . 6
⊢ (𝐴 ⊊ 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ ¬ 𝐴 = 𝐶)) |
11 | | dfpss2 4019 |
. . . . . 6
⊢ (𝐶 ⊊ 𝐵 ↔ (𝐶 ⊆ 𝐵 ∧ ¬ 𝐶 = 𝐵)) |
12 | 10, 11 | anbi12i 627 |
. . . . 5
⊢ ((𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵) ↔ ((𝐴 ⊆ 𝐶 ∧ ¬ 𝐴 = 𝐶) ∧ (𝐶 ⊆ 𝐵 ∧ ¬ 𝐶 = 𝐵))) |
13 | 3, 9, 12 | 3bitr4i 303 |
. . . 4
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) ∧ ¬ (𝐶 = 𝐴 ∨ 𝐶 = 𝐵)) ↔ (𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵)) |
14 | 13 | notbii 320 |
. . 3
⊢ (¬
((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) ∧ ¬ (𝐶 = 𝐴 ∨ 𝐶 = 𝐵)) ↔ ¬ (𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵)) |
15 | 2, 14 | bitr2i 275 |
. 2
⊢ (¬
(𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵) ↔ ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) → (𝐶 = 𝐴 ∨ 𝐶 = 𝐵))) |
16 | 1, 15 | syl6ib 250 |
1
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) → (𝐶 = 𝐴 ∨ 𝐶 = 𝐵)))) |