Metamath Proof Explorer

Theorem cvnbtwn3

Description: The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvnbtwn3 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ → A ⋖ ℋ B → A ⊆ C ∧ C ⊂ B → C = A

Proof

Step Hyp Ref Expression
1 cvnbtwn ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ → A ⋖ ℋ B → ¬ A ⊂ C ∧ C ⊂ B
2 iman ⊢ A ⊆ C ∧ C ⊂ B → A = C ↔ ¬ A ⊆ C ∧ C ⊂ B ∧ ¬ A = C
3 eqcom ⊢ C = A ↔ A = C
4 3 imbi2i ⊢ A ⊆ C ∧ C ⊂ B → C = A ↔ A ⊆ C ∧ C ⊂ B → A = C
5 dfpss2 ⊢ A ⊂ C ↔ A ⊆ C ∧ ¬ A = C
6 5 anbi1i ⊢ A ⊂ C ∧ C ⊂ B ↔ A ⊆ C ∧ ¬ A = C ∧ C ⊂ B
7 an32 ⊢ A ⊆ C ∧ ¬ A = C ∧ C ⊂ B ↔ A ⊆ C ∧ C ⊂ B ∧ ¬ A = C
8 6 7 bitri ⊢ A ⊂ C ∧ C ⊂ B ↔ A ⊆ C ∧ C ⊂ B ∧ ¬ A = C
9 8 notbii ⊢ ¬ A ⊂ C ∧ C ⊂ B ↔ ¬ A ⊆ C ∧ C ⊂ B ∧ ¬ A = C
10 2 4 9 3bitr4ri ⊢ ¬ A ⊂ C ∧ C ⊂ B ↔ A ⊆ C ∧ C ⊂ B → C = A
11 1 10 imbitrdi ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ → A ⋖ ℋ B → A ⊆ C ∧ C ⊂ B → C = A