Metamath Proof Explorer

Theorem cvnbtwn2

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

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

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 → C = B ↔ ¬ A ⊂ C ∧ C ⊆ B ∧ ¬ C = B
3 anass ⊢ A ⊂ C ∧ C ⊆ B ∧ ¬ C = B ↔ A ⊂ C ∧ C ⊆ B ∧ ¬ C = B
4 dfpss2 ⊢ C ⊂ B ↔ C ⊆ B ∧ ¬ C = B
5 4 anbi2i ⊢ A ⊂ C ∧ C ⊂ B ↔ A ⊂ C ∧ C ⊆ B ∧ ¬ C = B
6 3 5 bitr4i ⊢ A ⊂ C ∧ C ⊆ B ∧ ¬ C = B ↔ A ⊂ C ∧ C ⊂ B
7 6 notbii ⊢ ¬ A ⊂ C ∧ C ⊆ B ∧ ¬ C = B ↔ ¬ A ⊂ C ∧ C ⊂ B
8 2 7 bitr2i ⊢ ¬ A ⊂ C ∧ C ⊂ B ↔ A ⊂ C ∧ C ⊆ B → C = B
9 1 8 imbitrdi ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ → A ⋖ ℋ B → A ⊂ C ∧ C ⊆ B → C = B