Theorem lcvpss

Description: The covers relation implies proper subset. ( cvpss analog.) (Contributed by NM, 7-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lcvfbr.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lcvfbr.c	⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
3		lcvfbr.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
4		lcvfbr.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
5		lcvfbr.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6		lcvpss.d	⊢ ( 𝜑 → 𝑇 𝐶 𝑈 )
7	1 2 3 4 5	lcvbr	⊢ ( 𝜑 → ( 𝑇 𝐶 𝑈 ↔ ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) ) )
8	6 7	mpbid	⊢ ( 𝜑 → ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) )
9	8	simpld	⊢ ( 𝜑 → 𝑇 ⊊ 𝑈 )