Theorem lcvnbtwn3

Description: The covers relation implies no in-betweenness. ( cvnbtwn3 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 )
	lcvnbtwn3.p	|- ( ph -> R C_ U )
	lcvnbtwn3.q	|- ( ph -> U C. T )
Assertion	lcvnbtwn3	|- ( ph -> U = R )

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		lcvnbtwn3.p	|- ( ph -> R C_ U )
9		lcvnbtwn3.q	|- ( ph -> U C. T )
10	1 2 3 4 5 6 7	lcvnbtwn	|- ( ph -> -. ( R C. U /\ U C. T ) )
11		iman	|- ( ( ( R C_ U /\ U C. T ) -> R = U ) <-> -. ( ( R C_ U /\ U C. T ) /\ -. R = U ) )
12		eqcom	|- ( U = R <-> R = U )
13	12	imbi2i	|- ( ( ( R C_ U /\ U C. T ) -> U = R ) <-> ( ( R C_ U /\ U C. T ) -> R = U ) )
14		dfpss2	|- ( R C. U <-> ( R C_ U /\ -. R = U ) )
15	14	anbi1i	|- ( ( R C. U /\ U C. T ) <-> ( ( R C_ U /\ -. R = U ) /\ U C. T ) )
16		an32	|- ( ( ( R C_ U /\ -. R = U ) /\ U C. T ) <-> ( ( R C_ U /\ U C. T ) /\ -. R = U ) )
17	15 16	bitri	|- ( ( R C. U /\ U C. T ) <-> ( ( R C_ U /\ U C. T ) /\ -. R = U ) )
18	17	notbii	|- ( -. ( R C. U /\ U C. T ) <-> -. ( ( R C_ U /\ U C. T ) /\ -. R = U ) )
19	11 13 18	3bitr4ri	|- ( -. ( R C. U /\ U C. T ) <-> ( ( R C_ U /\ U C. T ) -> U = R ) )
20	10 19	sylib	|- ( ph -> ( ( R C_ U /\ U C. T ) -> U = R ) )
21	8 9 20	mp2and	|- ( ph -> U = R )