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

Metamath Proof Explorer

Theorem cvnbtwn4

Description: The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of MaedaMaeda p. 31. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cvnbtwn ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) )
2 iman ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) ) ↔ ¬ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ∧ ¬ ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) ) )
3 an4 ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ∧ ( ¬ 𝐴 = 𝐶 ∧ ¬ 𝐶 = 𝐵 ) ) ↔ ( ( 𝐴 ⊆ 𝐶 ∧ ¬ 𝐴 = 𝐶 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ ¬ 𝐶 = 𝐵 ) ) )
4 ioran ⊢ ( ¬ ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) ↔ ( ¬ 𝐶 = 𝐴 ∧ ¬ 𝐶 = 𝐵 ) )
5 eqcom ⊢ ( 𝐶 = 𝐴 ↔ 𝐴 = 𝐶 )
6 5 notbii ⊢ ( ¬ 𝐶 = 𝐴 ↔ ¬ 𝐴 = 𝐶 )
7 6 anbi1i ⊢ ( ( ¬ 𝐶 = 𝐴 ∧ ¬ 𝐶 = 𝐵 ) ↔ ( ¬ 𝐴 = 𝐶 ∧ ¬ 𝐶 = 𝐵 ) )
8 4 7 bitri ⊢ ( ¬ ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) ↔ ( ¬ 𝐴 = 𝐶 ∧ ¬ 𝐶 = 𝐵 ) )
9 8 anbi2i ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ∧ ¬ ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) ) ↔ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ∧ ( ¬ 𝐴 = 𝐶 ∧ ¬ 𝐶 = 𝐵 ) ) )
10 dfpss2 ⊢ ( 𝐴 ⊊ 𝐶 ↔ ( 𝐴 ⊆ 𝐶 ∧ ¬ 𝐴 = 𝐶 ) )
11 dfpss2 ⊢ ( 𝐶 ⊊ 𝐵 ↔ ( 𝐶 ⊆ 𝐵 ∧ ¬ 𝐶 = 𝐵 ) )
12 10 11 anbi12i ⊢ ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ↔ ( ( 𝐴 ⊆ 𝐶 ∧ ¬ 𝐴 = 𝐶 ) ∧ ( 𝐶 ⊆ 𝐵 ∧ ¬ 𝐶 = 𝐵 ) ) )
13 3 9 12 3bitr4i ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ∧ ¬ ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) ) ↔ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) )
14 13 notbii ⊢ ( ¬ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ∧ ¬ ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) ) ↔ ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) )
15 2 14 bitr2i ⊢ ( ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ↔ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) ) )
16 1 15 imbitrdi ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → ( 𝐶 = 𝐴 ∨ 𝐶 = 𝐵 ) ) ) )