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 ⊢ S = LSubSp ⁡ W
lcvfbr.c ⊢ C = ⋖ L ⁡ W
lcvfbr.w ⊢ φ → W ∈ X
lcvfbr.t ⊢ φ → T ∈ S
lcvfbr.u ⊢ φ → U ∈ S
lcvpss.d ⊢ φ → T C U
Assertion lcvpss ⊢ φ → T ⊂ U

Proof

Step Hyp Ref Expression
1 lcvfbr.s ⊢ S = LSubSp ⁡ W
2 lcvfbr.c ⊢ C = ⋖ L ⁡ W
3 lcvfbr.w ⊢ φ → W ∈ X
4 lcvfbr.t ⊢ φ → T ∈ S
5 lcvfbr.u ⊢ φ → U ∈ S
6 lcvpss.d ⊢ φ → T C U
7 1 2 3 4 5 lcvbr ⊢ φ → T C U ↔ T ⊂ U ∧ ¬ ∃ s ∈ S T ⊂ s ∧ s ⊂ U
8 6 7 mpbid ⊢ φ → T ⊂ U ∧ ¬ ∃ s ∈ S T ⊂ s ∧ s ⊂ U
9 8 simpld ⊢ φ → T ⊂ U