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 e. (/)
2 base0 
 |-  (/) = ( Base ` (/) )
3 eqid 
 |-  ( LSubSp ` (/) ) = ( LSubSp ` (/) )
4 2 3 lssss 
 |-  ( a e. ( LSubSp ` (/) ) -> a C_ (/) )
5 ss0 
 |-  ( a C_ (/) -> a = (/) )
6 4 5 syl 
 |-  ( a e. ( LSubSp ` (/) ) -> a = (/) )
7 3 lssn0 
 |-  ( a e. ( LSubSp ` (/) ) -> a =/= (/) )
8 7 neneqd 
 |-  ( a e. ( LSubSp ` (/) ) -> -. a = (/) )
9 6 8 pm2.65i 
 |-  -. a e. ( LSubSp ` (/) )
10 1 9 2false 
 |-  ( a e. (/) <-> a e. ( LSubSp ` (/) ) )
11 10 eqriv 
 |-  (/) = ( LSubSp ` (/) )