This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ( 𝐶 ∈ Cℋ → ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) ) )
10 9 com23 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐶 ∈ Cℋ → ( 𝐴 ⋖ℋ 𝐵 → ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) ) )
11 10 3impia ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) )