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

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

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 lcvnbtwn2.p ⊢ ( 𝜑 → 𝑅 ⊊ 𝑈 )
9 lcvnbtwn2.q ⊢ ( 𝜑 → 𝑈 ⊆ 𝑇 )
10 1 2 3 4 5 6 7 lcvnbtwn ⊢ ( 𝜑 → ¬ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) )
11 iman ⊢ ( ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) → 𝑈 = 𝑇 ) ↔ ¬ ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) ∧ ¬ 𝑈 = 𝑇 ) )
12 anass ⊢ ( ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) ∧ ¬ 𝑈 = 𝑇 ) ↔ ( 𝑅 ⊊ 𝑈 ∧ ( 𝑈 ⊆ 𝑇 ∧ ¬ 𝑈 = 𝑇 ) ) )
13 dfpss2 ⊢ ( 𝑈 ⊊ 𝑇 ↔ ( 𝑈 ⊆ 𝑇 ∧ ¬ 𝑈 = 𝑇 ) )
14 13 anbi2i ⊢ ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ↔ ( 𝑅 ⊊ 𝑈 ∧ ( 𝑈 ⊆ 𝑇 ∧ ¬ 𝑈 = 𝑇 ) ) )
15 12 14 bitr4i ⊢ ( ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) ∧ ¬ 𝑈 = 𝑇 ) ↔ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) )
16 15 notbii ⊢ ( ¬ ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) ∧ ¬ 𝑈 = 𝑇 ) ↔ ¬ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) )
17 11 16 bitr2i ⊢ ( ¬ ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊊ 𝑇 ) ↔ ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) → 𝑈 = 𝑇 ) )
18 10 17 sylib ⊢ ( 𝜑 → ( ( 𝑅 ⊊ 𝑈 ∧ 𝑈 ⊆ 𝑇 ) → 𝑈 = 𝑇 ) )
19 8 9 18 mp2and ⊢ ( 𝜑 → 𝑈 = 𝑇 )