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

Metamath Proof Explorer

Theorem cvnbtwn2

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

Ref Expression
Assertion cvnbtwn2 ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 cvnbtwn ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) )
2 iman ⊢ ( ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 = 𝐵 ) ↔ ¬ ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ∧ ¬ 𝐶 = 𝐵 ) )
3 anass ⊢ ( ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ∧ ¬ 𝐶 = 𝐵 ) ↔ ( 𝐴 ⊊ 𝐶 ∧ ( 𝐶 ⊆ 𝐵 ∧ ¬ 𝐶 = 𝐵 ) ) )
4 dfpss2 ⊢ ( 𝐶 ⊊ 𝐵 ↔ ( 𝐶 ⊆ 𝐵 ∧ ¬ 𝐶 = 𝐵 ) )
5 4 anbi2i ⊢ ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ↔ ( 𝐴 ⊊ 𝐶 ∧ ( 𝐶 ⊆ 𝐵 ∧ ¬ 𝐶 = 𝐵 ) ) )
6 3 5 bitr4i ⊢ ( ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ∧ ¬ 𝐶 = 𝐵 ) ↔ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) )
7 6 notbii ⊢ ( ¬ ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ∧ ¬ 𝐶 = 𝐵 ) ↔ ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) )
8 2 7 bitr2i ⊢ ( ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ↔ ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 = 𝐵 ) )
9 1 8 imbitrdi ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 = 𝐵 ) ) )