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