Theorem lcvpss

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

	Ref	Expression
Hypotheses	lcvfbr.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lcvfbr.c	$$⊢C={⋖}_L\left(W\right)$$
	lcvfbr.w	$$⊢\phi \to W\in X$$
	lcvfbr.t	$$⊢\phi \to T\in S$$
	lcvfbr.u	$$⊢\phi \to U\in S$$
	lcvpss.d	$$⊢\phi \to TCU$$
Assertion	lcvpss	$$⊢\phi \to T\subset U$$

Proof

Step	Hyp	Ref	Expression
1		lcvfbr.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lcvfbr.c	$$⊢C={⋖}_L\left(W\right)$$
3		lcvfbr.w	$$⊢\phi \to W\in X$$
4		lcvfbr.t	$$⊢\phi \to T\in S$$
5		lcvfbr.u	$$⊢\phi \to U\in S$$
6		lcvpss.d	$$⊢\phi \to TCU$$
7	1 2 3 4 5	lcvbr	$$⊢\phi \to \left(TCU\leftrightarrow \left(T\subset U\wedge \neg \exists s\in S\left(T\subset s\wedge s\subset U\right)\right)\right)$$
8	6 7	mpbid	$$⊢\phi \to \left(T\subset U\wedge \neg \exists s\in S\left(T\subset s\wedge s\subset U\right)\right)$$
9	8	simpld	$$⊢\phi \to T\subset U$$