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	⊢ ¬ 𝑎 ∈ ∅
2		base0	⊢ ∅ = ( Base ‘ ∅ )
3		eqid	⊢ ( LSubSp ‘ ∅ ) = ( LSubSp ‘ ∅ )
4	2 3	lssss	⊢ ( 𝑎 ∈ ( LSubSp ‘ ∅ ) → 𝑎 ⊆ ∅ )
5		ss0	⊢ ( 𝑎 ⊆ ∅ → 𝑎 = ∅ )
6	4 5	syl	⊢ ( 𝑎 ∈ ( LSubSp ‘ ∅ ) → 𝑎 = ∅ )
7	3	lssn0	⊢ ( 𝑎 ∈ ( LSubSp ‘ ∅ ) → 𝑎 ≠ ∅ )
8	7	neneqd	⊢ ( 𝑎 ∈ ( LSubSp ‘ ∅ ) → ¬ 𝑎 = ∅ )
9	6 8	pm2.65i	⊢ ¬ 𝑎 ∈ ( LSubSp ‘ ∅ )
10	1 9	2false	⊢ ( 𝑎 ∈ ∅ ↔ 𝑎 ∈ ( LSubSp ‘ ∅ ) )
11	10	eqriv	⊢ ∅ = ( LSubSp ‘ ∅ )