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 syl6bi ⊢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