lcvnbtwn3

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

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		lcvnbtwn3.p	⊢ ( 𝜑 → 𝑅 ⊆ 𝑈 )
9		lcvnbtwn3.q	⊢ ( 𝜑 → 𝑈 ⊊ 𝑇 )
10	1 2 3 4 5 6 7	lcvnbtwn	⊢ ( 𝜑 → ¬ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) )
11		iman	⊢ ( ( ( 𝑅 ⊆ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) → 𝑅 = 𝑈 ) ↔ ¬ ( ( 𝑅 ⊆ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ∧ ¬ 𝑅 = 𝑈 ) )
12		eqcom	⊢ ( 𝑈 = 𝑅 ↔ 𝑅 = 𝑈 )
13	12	imbi2i	⊢ ( ( ( 𝑅 ⊆ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) → 𝑈 = 𝑅 ) ↔ ( ( 𝑅 ⊆ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) → 𝑅 = 𝑈 ) )
14		dfpss2	⊢ ( 𝑅 ⊊ 𝑈 ↔ ( 𝑅 ⊆ 𝑈 ∧ ¬ 𝑅 = 𝑈 ) )
15	14	anbi1i	⊢ ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ↔ ( ( 𝑅 ⊆ 𝑈 ∧ ¬ 𝑅 = 𝑈 ) ∧ 𝑈 ⊊ 𝑇 ) )
16		an32	⊢ ( ( ( 𝑅 ⊆ 𝑈 ∧ ¬ 𝑅 = 𝑈 ) ∧ 𝑈 ⊊ 𝑇 ) ↔ ( ( 𝑅 ⊆ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ∧ ¬ 𝑅 = 𝑈 ) )
17	15 16	bitri	⊢ ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ↔ ( ( 𝑅 ⊆ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ∧ ¬ 𝑅 = 𝑈 ) )
18	17	notbii	⊢ ( ¬ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ↔ ¬ ( ( 𝑅 ⊆ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ∧ ¬ 𝑅 = 𝑈 ) )
19	11 13 18	3bitr4ri	⊢ ( ¬ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ↔ ( ( 𝑅 ⊆ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) → 𝑈 = 𝑅 ) )
20	10 19	sylib	⊢ ( 𝜑 → ( ( 𝑅 ⊆ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) → 𝑈 = 𝑅 ) )
21	8 9 20	mp2and	⊢ ( 𝜑 → 𝑈 = 𝑅 )

Metamath Proof Explorer

Theorem lcvnbtwn3

Proof