Theorem lcvnbtwn2

Description: The covers relation implies no in-betweenness. ( cvnbtwn2 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	⊢ ( 𝜑 → 𝑅 𝐶 𝑇 )
	lcvnbtwn2.p	⊢ ( 𝜑 → 𝑅 ⊊ 𝑈 )
	lcvnbtwn2.q	⊢ ( 𝜑 → 𝑈 ⊆ 𝑇 )
Assertion	lcvnbtwn2	⊢ ( 𝜑 → 𝑈 = 𝑇 )

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		lcvnbtwn2.p	⊢ ( 𝜑 → 𝑅 ⊊ 𝑈 )
9		lcvnbtwn2.q	⊢ ( 𝜑 → 𝑈 ⊆ 𝑇 )
10	1 2 3 4 5 6 7	lcvnbtwn	⊢ ( 𝜑 → ¬ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) )
11		iman	⊢ ( ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) → 𝑈 = 𝑇 ) ↔ ¬ ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) ∧ ¬ 𝑈 = 𝑇 ) )
12		anass	⊢ ( ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) ∧ ¬ 𝑈 = 𝑇 ) ↔ ( 𝑅 ⊊ 𝑈 ∧ ( 𝑈 ⊆ 𝑇 ∧ ¬ 𝑈 = 𝑇 ) ) )
13		dfpss2	⊢ ( 𝑈 ⊊ 𝑇 ↔ ( 𝑈 ⊆ 𝑇 ∧ ¬ 𝑈 = 𝑇 ) )
14	13	anbi2i	⊢ ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ↔ ( 𝑅 ⊊ 𝑈 ∧ ( 𝑈 ⊆ 𝑇 ∧ ¬ 𝑈 = 𝑇 ) ) )
15	12 14	bitr4i	⊢ ( ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) ∧ ¬ 𝑈 = 𝑇 ) ↔ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) )
16	15	notbii	⊢ ( ¬ ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) ∧ ¬ 𝑈 = 𝑇 ) ↔ ¬ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) )
17	11 16	bitr2i	⊢ ( ¬ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ↔ ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) → 𝑈 = 𝑇 ) )
18	10 17	sylib	⊢ ( 𝜑 → ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) → 𝑈 = 𝑇 ) )
19	8 9 18	mp2and	⊢ ( 𝜑 → 𝑈 = 𝑇 )