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ℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 = 𝐵 ) ) )