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

Metamath Proof Explorer

Theorem cvnbtwn3

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

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

Proof

Step Hyp Ref Expression
1 cvnbtwn ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) )
2 iman ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) → 𝐴 = 𝐶 ) ↔ ¬ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ∧ ¬ 𝐴 = 𝐶 ) )
3 eqcom ⊢ ( 𝐶 = 𝐴 ↔ 𝐴 = 𝐶 )
4 3 imbi2i ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) → 𝐶 = 𝐴 ) ↔ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) → 𝐴 = 𝐶 ) )
5 dfpss2 ⊢ ( 𝐴 ⊊ 𝐶 ↔ ( 𝐴 ⊆ 𝐶 ∧ ¬ 𝐴 = 𝐶 ) )
6 5 anbi1i ⊢ ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ↔ ( ( 𝐴 ⊆ 𝐶 ∧ ¬ 𝐴 = 𝐶 ) ∧ 𝐶 ⊊ 𝐵 ) )
7 an32 ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ ¬ 𝐴 = 𝐶 ) ∧ 𝐶 ⊊ 𝐵 ) ↔ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ∧ ¬ 𝐴 = 𝐶 ) )
8 6 7 bitri ⊢ ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ↔ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ∧ ¬ 𝐴 = 𝐶 ) )
9 8 notbii ⊢ ( ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ↔ ¬ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ∧ ¬ 𝐴 = 𝐶 ) )
10 2 4 9 3bitr4ri ⊢ ( ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ↔ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) → 𝐶 = 𝐴 ) )
11 1 10 imbitrdi ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) → 𝐶 = 𝐴 ) ) )