This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → ¬ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) )