Theorem lcvnbtwn

Description: The covers relation implies no in-betweenness. ( cvnbtwn analog.) (Contributed by NM, 7-Jan-2015)

	Ref	Expression
Hypotheses	lcvnbtwn.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lcvnbtwn.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
	lcvnbtwn.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
	lcvnbtwn.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
	lcvnbtwn.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
	lcvnbtwn.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	lcvnbtwn.d	⊢ ( 𝜑 → 𝑅 𝐶 𝑇 )
Assertion	lcvnbtwn	⊢ ( 𝜑 → ¬ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		lcvnbtwn.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lcvnbtwn.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
3		lcvnbtwn.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
4		lcvnbtwn.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
5		lcvnbtwn.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
6		lcvnbtwn.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7		lcvnbtwn.d	⊢ ( 𝜑 → 𝑅 𝐶 𝑇 )
8	1 2 3 4 5	lcvbr	⊢ ( 𝜑 → ( 𝑅 𝐶 𝑇 ↔ ( 𝑅 ⊊ 𝑇 ∧ ¬ ∃ 𝑢 ∈ 𝑆 ( 𝑅 ⊊ 𝑢 ∧ 𝑢 ⊊ 𝑇 ) ) ) )
9	7 8	mpbid	⊢ ( 𝜑 → ( 𝑅 ⊊ 𝑇 ∧ ¬ ∃ 𝑢 ∈ 𝑆 ( 𝑅 ⊊ 𝑢 ∧ 𝑢 ⊊ 𝑇 ) ) )
10	9	simprd	⊢ ( 𝜑 → ¬ ∃ 𝑢 ∈ 𝑆 ( 𝑅 ⊊ 𝑢 ∧ 𝑢 ⊊ 𝑇 ) )
11		psseq2	⊢ ( 𝑢 = 𝑈 → ( 𝑅 ⊊ 𝑢 ↔ 𝑅 ⊊ 𝑈 ) )
12		psseq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 ⊊ 𝑇 ↔ 𝑈 ⊊ 𝑇 ) )
13	11 12	anbi12d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑅 ⊊ 𝑢 ∧ 𝑢 ⊊ 𝑇 ) ↔ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ) )
14	13	rspcev	⊢ ( ( 𝑈 ∈ 𝑆 ∧ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝑅 ⊊ 𝑢 ∧ 𝑢 ⊊ 𝑇 ) )
15	6 14	sylan	⊢ ( ( 𝜑 ∧ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝑅 ⊊ 𝑢 ∧ 𝑢 ⊊ 𝑇 ) )
16	10 15	mtand	⊢ ( 𝜑 → ¬ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) )