Metamath Proof Explorer


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

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