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

Metamath Proof Explorer

Theorem lcvpss

Description: The covers relation implies proper subset. ( cvpss analog.) (Contributed by NM, 7-Jan-2015)

Ref Expression
Hypotheses lcvfbr.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lcvfbr.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
lcvfbr.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
lcvfbr.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
lcvfbr.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lcvpss.d ⊢ ( 𝜑 → 𝑇 𝐶 𝑈 )
Assertion lcvpss ( 𝜑 → 𝑇 ⊊ 𝑈 )

Proof

Step Hyp Ref Expression
1 lcvfbr.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lcvfbr.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
3 lcvfbr.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
4 lcvfbr.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
5 lcvfbr.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6 lcvpss.d ⊢ ( 𝜑 → 𝑇 𝐶 𝑈 )
7 1 2 3 4 5 lcvbr ⊢ ( 𝜑 → ( 𝑇 𝐶 𝑈 ↔ ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) ) )
8 6 7 mpbid ⊢ ( 𝜑 → ( 𝑇 ⊊ 𝑈 ∧ ¬ ∃ 𝑠 ∈ 𝑆 ( 𝑇 ⊊ 𝑠 ∧ 𝑠 ⊊ 𝑈 ) ) )
9 8 simpld ⊢ ( 𝜑 → 𝑇 ⊊ 𝑈 )