Theorem cvrnbtwn

Description: There is no element between the two arguments of the covers relation. ( cvnbtwn analog.) (Contributed by NM, 18-Oct-2011)

	Ref	Expression
Hypotheses	cvrfval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cvrfval.s	⊢ < = ( lt ‘ 𝐾 )
	cvrfval.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion	cvrnbtwn	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		cvrfval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cvrfval.s	⊢ < = ( lt ‘ 𝐾 )
3		cvrfval.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4	1 2 3	cvrval	⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 < 𝑌 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) ) )
5	4	3adant3r3	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 < 𝑌 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) ) )
6		ralnex	⊢ ( ∀ 𝑧 ∈ 𝐵 ¬ ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ↔ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) )
7		breq2	⊢ ( 𝑧 = 𝑍 → ( 𝑋 < 𝑧 ↔ 𝑋 < 𝑍 ) )
8		breq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 < 𝑌 ↔ 𝑍 < 𝑌 ) )
9	7 8	anbi12d	⊢ ( 𝑧 = 𝑍 → ( ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ↔ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ) )
10	9	notbid	⊢ ( 𝑧 = 𝑍 → ( ¬ ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ↔ ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ) )
11	10	rspcv	⊢ ( 𝑍 ∈ 𝐵 → ( ∀ 𝑧 ∈ 𝐵 ¬ ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) → ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ) )
12	6 11	syl5bir	⊢ ( 𝑍 ∈ 𝐵 → ( ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) → ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ) )
13	12	adantld	⊢ ( 𝑍 ∈ 𝐵 → ( ( 𝑋 < 𝑌 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) → ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ) )
14	13	3ad2ant3	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 < 𝑌 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) → ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ) )
15	14	adantl	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 < 𝑌 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) → ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ) )
16	5 15	sylbid	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 → ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ) )
17	16	3impia	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) )