Theorem lcvnbtwn

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

	Ref	Expression
Hypotheses	lcvnbtwn.s	|- S = ( LSubSp ` W )
	lcvnbtwn.c	|- C = (
	lcvnbtwn.w	|- ( ph -> W e. X )
	lcvnbtwn.r	|- ( ph -> R e. S )
	lcvnbtwn.t	|- ( ph -> T e. S )
	lcvnbtwn.u	|- ( ph -> U e. S )
	lcvnbtwn.d	|- ( ph -> R C T )
Assertion	lcvnbtwn	|- ( ph -> -. ( R C. U /\ U C. T ) )

Proof

Step	Hyp	Ref	Expression
1		lcvnbtwn.s	|- S = ( LSubSp ` W )
2		lcvnbtwn.c	|- C = (
3		lcvnbtwn.w	|- ( ph -> W e. X )
4		lcvnbtwn.r	|- ( ph -> R e. S )
5		lcvnbtwn.t	|- ( ph -> T e. S )
6		lcvnbtwn.u	|- ( ph -> U e. S )
7		lcvnbtwn.d	|- ( ph -> R C T )
8	1 2 3 4 5	lcvbr	|- ( ph -> ( R C T <-> ( R C. T /\ -. E. u e. S ( R C. u /\ u C. T ) ) ) )
9	7 8	mpbid	|- ( ph -> ( R C. T /\ -. E. u e. S ( R C. u /\ u C. T ) ) )
10	9	simprd	|- ( ph -> -. E. u e. S ( R C. u /\ u C. T ) )
11		psseq2	|- ( u = U -> ( R C. u <-> R C. U ) )
12		psseq1	|- ( u = U -> ( u C. T <-> U C. T ) )
13	11 12	anbi12d	|- ( u = U -> ( ( R C. u /\ u C. T ) <-> ( R C. U /\ U C. T ) ) )
14	13	rspcev	|- ( ( U e. S /\ ( R C. U /\ U C. T ) ) -> E. u e. S ( R C. u /\ u C. T ) )
15	6 14	sylan	|- ( ( ph /\ ( R C. U /\ U C. T ) ) -> E. u e. S ( R C. u /\ u C. T ) )
16	10 15	mtand	|- ( ph -> -. ( R C. U /\ U C. T ) )