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 aLSubSpa
5 ss0 aa=
6 4 5 syl aLSubSpa=
7 3 lssn0 aLSubSpa
8 7 neneqd aLSubSp¬a=
9 6 8 pm2.65i ¬aLSubSp
10 1 9 2false aaLSubSp
11 10 eqriv =LSubSp