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

Metamath Proof Explorer

Theorem 00lss

Description: The empty structure has no subspaces (for use with fvco4i ). (Contributed by Stefan O'Rear, 31-Mar-2015)

Ref Expression
Assertion 00lss ⊢ ∅ = LSubSp ⁡ ∅

Proof

Step Hyp Ref Expression
1 noel ⊢ ¬ a ∈ ∅
2 base0 ⊢ ∅ = Base ∅
3 eqid ⊢ LSubSp ⁡ ∅ = LSubSp ⁡ ∅
4 2 3 lssss ⊢ a ∈ LSubSp ⁡ ∅ → a ⊆ ∅
5 ss0 ⊢ a ⊆ ∅ → a = ∅
6 4 5 syl ⊢ a ∈ LSubSp ⁡ ∅ → a = ∅
7 3 lssn0 ⊢ a ∈ LSubSp ⁡ ∅ → a ≠ ∅
8 7 neneqd ⊢ a ∈ LSubSp ⁡ ∅ → ¬ a = ∅
9 6 8 pm2.65i ⊢ ¬ a ∈ LSubSp ⁡ ∅
10 1 9 2false ⊢ a ∈ ∅ ↔ a ∈ LSubSp ⁡ ∅
11 10 eqriv ⊢ ∅ = LSubSp ⁡ ∅