Metamath Proof Explorer


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 = L W
lcvnbtwn.w φ W X
lcvnbtwn.r φ R S
lcvnbtwn.t φ T S
lcvnbtwn.u φ U S
lcvnbtwn.d φ R C T
lcvnbtwn2.p φ R U
lcvnbtwn2.q φ U T
Assertion lcvnbtwn2 φ U = T

Proof

Step Hyp Ref Expression
1 lcvnbtwn.s S = LSubSp W
2 lcvnbtwn.c C = L W
3 lcvnbtwn.w φ W X
4 lcvnbtwn.r φ R S
5 lcvnbtwn.t φ T S
6 lcvnbtwn.u φ U S
7 lcvnbtwn.d φ R C T
8 lcvnbtwn2.p φ R U
9 lcvnbtwn2.q φ U T
10 1 2 3 4 5 6 7 lcvnbtwn φ ¬ R U U T
11 iman R U U T U = T ¬ R U U T ¬ U = T
12 anass R U U T ¬ U = T R U U T ¬ U = T
13 dfpss2 U T U T ¬ U = T
14 13 anbi2i R U U T R U U T ¬ U = T
15 12 14 bitr4i R U U T ¬ U = T R U U T
16 15 notbii ¬ R U U T ¬ U = T ¬ R U U T
17 11 16 bitr2i ¬ R U U T R U U T U = T
18 10 17 sylib φ R U U T U = T
19 8 9 18 mp2and φ U = T