Metamath Proof Explorer

Theorem cvnbtwn

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

Ref Expression
Assertion cvnbtwn ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ → A ⋖ ℋ B → ¬ A ⊂ C ∧ C ⊂ B

Proof

Step Hyp Ref Expression
1 cvbr ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ B ↔ A ⊂ B ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B
2 psseq2 ⊢ x = C → A ⊂ x ↔ A ⊂ C
3 psseq1 ⊢ x = C → x ⊂ B ↔ C ⊂ B
4 2 3 anbi12d ⊢ x = C → A ⊂ x ∧ x ⊂ B ↔ A ⊂ C ∧ C ⊂ B
5 4 rspcev ⊢ C ∈ C ℋ ∧ A ⊂ C ∧ C ⊂ B → ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B
6 5 ex ⊢ C ∈ C ℋ → A ⊂ C ∧ C ⊂ B → ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B
7 6 con3rr3 ⊢ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B → C ∈ C ℋ → ¬ A ⊂ C ∧ C ⊂ B
8 7 adantl ⊢ A ⊂ B ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B → C ∈ C ℋ → ¬ A ⊂ C ∧ C ⊂ B
9 1 8 biimtrdi ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ B → C ∈ C ℋ → ¬ A ⊂ C ∧ C ⊂ B
10 9 com23 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → C ∈ C ℋ → A ⋖ ℋ B → ¬ A ⊂ C ∧ C ⊂ B
11 10 3impia ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ → A ⋖ ℋ B → ¬ A ⊂ C ∧ C ⊂ B