Metamath Proof Explorer


Theorem lcvnbtwn

Description: The covers relation implies no in-betweenness. ( cvnbtwn 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 ( 𝜑𝑅 𝐶 𝑇 )
Assertion lcvnbtwn ( 𝜑 → ¬ ( 𝑅𝑈𝑈𝑇 ) )

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 1 2 3 4 5 lcvbr ( 𝜑 → ( 𝑅 𝐶 𝑇 ↔ ( 𝑅𝑇 ∧ ¬ ∃ 𝑢𝑆 ( 𝑅𝑢𝑢𝑇 ) ) ) )
9 7 8 mpbid ( 𝜑 → ( 𝑅𝑇 ∧ ¬ ∃ 𝑢𝑆 ( 𝑅𝑢𝑢𝑇 ) ) )
10 9 simprd ( 𝜑 → ¬ ∃ 𝑢𝑆 ( 𝑅𝑢𝑢𝑇 ) )
11 psseq2 ( 𝑢 = 𝑈 → ( 𝑅𝑢𝑅𝑈 ) )
12 psseq1 ( 𝑢 = 𝑈 → ( 𝑢𝑇𝑈𝑇 ) )
13 11 12 anbi12d ( 𝑢 = 𝑈 → ( ( 𝑅𝑢𝑢𝑇 ) ↔ ( 𝑅𝑈𝑈𝑇 ) ) )
14 13 rspcev ( ( 𝑈𝑆 ∧ ( 𝑅𝑈𝑈𝑇 ) ) → ∃ 𝑢𝑆 ( 𝑅𝑢𝑢𝑇 ) )
15 6 14 sylan ( ( 𝜑 ∧ ( 𝑅𝑈𝑈𝑇 ) ) → ∃ 𝑢𝑆 ( 𝑅𝑢𝑢𝑇 ) )
16 10 15 mtand ( 𝜑 → ¬ ( 𝑅𝑈𝑈𝑇 ) )