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 𝑆 = ( LSubSp ‘ 𝑊 )
lcvnbtwn.c 𝐶 = ( ⋖L𝑊 )
lcvnbtwn.w ( 𝜑𝑊𝑋 )
lcvnbtwn.r ( 𝜑𝑅𝑆 )
lcvnbtwn.t ( 𝜑𝑇𝑆 )
lcvnbtwn.u ( 𝜑𝑈𝑆 )
lcvnbtwn.d ( 𝜑𝑅 𝐶 𝑇 )
lcvnbtwn3.p ( 𝜑𝑅𝑈 )
lcvnbtwn3.q ( 𝜑𝑈𝑇 )
Assertion lcvnbtwn3 ( 𝜑𝑈 = 𝑅 )

Proof

Step Hyp Ref Expression
1 lcvnbtwn.s 𝑆 = ( LSubSp ‘ 𝑊 )
2 lcvnbtwn.c 𝐶 = ( ⋖L𝑊 )
3 lcvnbtwn.w ( 𝜑𝑊𝑋 )
4 lcvnbtwn.r ( 𝜑𝑅𝑆 )
5 lcvnbtwn.t ( 𝜑𝑇𝑆 )
6 lcvnbtwn.u ( 𝜑𝑈𝑆 )
7 lcvnbtwn.d ( 𝜑𝑅 𝐶 𝑇 )
8 lcvnbtwn3.p ( 𝜑𝑅𝑈 )
9 lcvnbtwn3.q ( 𝜑𝑈𝑇 )
10 1 2 3 4 5 6 7 lcvnbtwn ( 𝜑 → ¬ ( 𝑅𝑈𝑈𝑇 ) )
11 iman ( ( ( 𝑅𝑈𝑈𝑇 ) → 𝑅 = 𝑈 ) ↔ ¬ ( ( 𝑅𝑈𝑈𝑇 ) ∧ ¬ 𝑅 = 𝑈 ) )
12 eqcom ( 𝑈 = 𝑅𝑅 = 𝑈 )
13 12 imbi2i ( ( ( 𝑅𝑈𝑈𝑇 ) → 𝑈 = 𝑅 ) ↔ ( ( 𝑅𝑈𝑈𝑇 ) → 𝑅 = 𝑈 ) )
14 dfpss2 ( 𝑅𝑈 ↔ ( 𝑅𝑈 ∧ ¬ 𝑅 = 𝑈 ) )
15 14 anbi1i ( ( 𝑅𝑈𝑈𝑇 ) ↔ ( ( 𝑅𝑈 ∧ ¬ 𝑅 = 𝑈 ) ∧ 𝑈𝑇 ) )
16 an32 ( ( ( 𝑅𝑈 ∧ ¬ 𝑅 = 𝑈 ) ∧ 𝑈𝑇 ) ↔ ( ( 𝑅𝑈𝑈𝑇 ) ∧ ¬ 𝑅 = 𝑈 ) )
17 15 16 bitri ( ( 𝑅𝑈𝑈𝑇 ) ↔ ( ( 𝑅𝑈𝑈𝑇 ) ∧ ¬ 𝑅 = 𝑈 ) )
18 17 notbii ( ¬ ( 𝑅𝑈𝑈𝑇 ) ↔ ¬ ( ( 𝑅𝑈𝑈𝑇 ) ∧ ¬ 𝑅 = 𝑈 ) )
19 11 13 18 3bitr4ri ( ¬ ( 𝑅𝑈𝑈𝑇 ) ↔ ( ( 𝑅𝑈𝑈𝑇 ) → 𝑈 = 𝑅 ) )
20 10 19 sylib ( 𝜑 → ( ( 𝑅𝑈𝑈𝑇 ) → 𝑈 = 𝑅 ) )
21 8 9 20 mp2and ( 𝜑𝑈 = 𝑅 )