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 e. CH /\ B e. CH /\ C e. CH ) -> ( A  -. ( A C. C /\ C C. B ) ) )

Proof

Step Hyp Ref Expression
1 cvbr 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A  ( A C. B /\ -. E. x e. CH ( A C. x /\ x C. B ) ) ) )
2 psseq2 
 |-  ( x = C -> ( A C. x <-> A C. C ) )
3 psseq1 
 |-  ( x = C -> ( x C. B <-> C C. B ) )
4 2 3 anbi12d 
 |-  ( x = C -> ( ( A C. x /\ x C. B ) <-> ( A C. C /\ C C. B ) ) )
5 4 rspcev 
 |-  ( ( C e. CH /\ ( A C. C /\ C C. B ) ) -> E. x e. CH ( A C. x /\ x C. B ) )
6 5 ex 
 |-  ( C e. CH -> ( ( A C. C /\ C C. B ) -> E. x e. CH ( A C. x /\ x C. B ) ) )
7 6 con3rr3 
 |-  ( -. E. x e. CH ( A C. x /\ x C. B ) -> ( C e. CH -> -. ( A C. C /\ C C. B ) ) )
8 7 adantl 
 |-  ( ( A C. B /\ -. E. x e. CH ( A C. x /\ x C. B ) ) -> ( C e. CH -> -. ( A C. C /\ C C. B ) ) )
9 1 8 biimtrdi 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A  ( C e. CH -> -. ( A C. C /\ C C. B ) ) ) )
10 9 com23 
 |-  ( ( A e. CH /\ B e. CH ) -> ( C e. CH -> ( A  -. ( A C. C /\ C C. B ) ) ) )
11 10 3impia 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A  -. ( A C. C /\ C C. B ) ) )