Theorem lcvnbtwn2

Description: The covers relation implies no in-betweenness. ( cvnbtwn2 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 )
	lcvnbtwn2.p	|- ( ph -> R C. U )
	lcvnbtwn2.q	|- ( ph -> U C_ T )
Assertion	lcvnbtwn2	|- ( ph -> U = 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		lcvnbtwn2.p	|- ( ph -> R C. U )
9		lcvnbtwn2.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 ) -> U = T ) <-> -. ( ( R C. U /\ U C_ T ) /\ -. U = T ) )
12		anass	|- ( ( ( R C. U /\ U C_ T ) /\ -. U = T ) <-> ( R C. U /\ ( U C_ T /\ -. U = T ) ) )
13		dfpss2	|- ( U C. T <-> ( U C_ T /\ -. U = T ) )
14	13	anbi2i	|- ( ( R C. U /\ U C. T ) <-> ( R C. U /\ ( U C_ T /\ -. U = T ) ) )
15	12 14	bitr4i	|- ( ( ( R C. U /\ U C_ T ) /\ -. U = T ) <-> ( R C. U /\ U C. T ) )
16	15	notbii	|- ( -. ( ( R C. U /\ U C_ T ) /\ -. U = T ) <-> -. ( R C. U /\ U C. T ) )
17	11 16	bitr2i	|- ( -. ( R C. U /\ U C. T ) <-> ( ( R C. U /\ U C_ T ) -> U = T ) )
18	10 17	sylib	|- ( ph -> ( ( R C. U /\ U C_ T ) -> U = T ) )
19	8 9 18	mp2and	|- ( ph -> U = T )