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 ( ( 𝐴C𝐵C𝐶C ) → ( 𝐴 𝐵 → ¬ ( 𝐴𝐶𝐶𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 cvbr ( ( 𝐴C𝐵C ) → ( 𝐴 𝐵 ↔ ( 𝐴𝐵 ∧ ¬ ∃ 𝑥C ( 𝐴𝑥𝑥𝐵 ) ) ) )
2 psseq2 ( 𝑥 = 𝐶 → ( 𝐴𝑥𝐴𝐶 ) )
3 psseq1 ( 𝑥 = 𝐶 → ( 𝑥𝐵𝐶𝐵 ) )
4 2 3 anbi12d ( 𝑥 = 𝐶 → ( ( 𝐴𝑥𝑥𝐵 ) ↔ ( 𝐴𝐶𝐶𝐵 ) ) )
5 4 rspcev ( ( 𝐶C ∧ ( 𝐴𝐶𝐶𝐵 ) ) → ∃ 𝑥C ( 𝐴𝑥𝑥𝐵 ) )
6 5 ex ( 𝐶C → ( ( 𝐴𝐶𝐶𝐵 ) → ∃ 𝑥C ( 𝐴𝑥𝑥𝐵 ) ) )
7 6 con3rr3 ( ¬ ∃ 𝑥C ( 𝐴𝑥𝑥𝐵 ) → ( 𝐶C → ¬ ( 𝐴𝐶𝐶𝐵 ) ) )
8 7 adantl ( ( 𝐴𝐵 ∧ ¬ ∃ 𝑥C ( 𝐴𝑥𝑥𝐵 ) ) → ( 𝐶C → ¬ ( 𝐴𝐶𝐶𝐵 ) ) )
9 1 8 syl6bi ( ( 𝐴C𝐵C ) → ( 𝐴 𝐵 → ( 𝐶C → ¬ ( 𝐴𝐶𝐶𝐵 ) ) ) )
10 9 com23 ( ( 𝐴C𝐵C ) → ( 𝐶C → ( 𝐴 𝐵 → ¬ ( 𝐴𝐶𝐶𝐵 ) ) ) )
11 10 3impia ( ( 𝐴C𝐵C𝐶C ) → ( 𝐴 𝐵 → ¬ ( 𝐴𝐶𝐶𝐵 ) ) )