Step |
Hyp |
Ref |
Expression |
1 |
|
lspsnid.v |
|- V = ( Base ` W ) |
2 |
|
lspsnid.n |
|- N = ( LSpan ` W ) |
3 |
|
snssi |
|- ( X e. V -> { X } C_ V ) |
4 |
1 2
|
lspssid |
|- ( ( W e. LMod /\ { X } C_ V ) -> { X } C_ ( N ` { X } ) ) |
5 |
3 4
|
sylan2 |
|- ( ( W e. LMod /\ X e. V ) -> { X } C_ ( N ` { X } ) ) |
6 |
|
snssg |
|- ( X e. V -> ( X e. ( N ` { X } ) <-> { X } C_ ( N ` { X } ) ) ) |
7 |
6
|
adantl |
|- ( ( W e. LMod /\ X e. V ) -> ( X e. ( N ` { X } ) <-> { X } C_ ( N ` { X } ) ) ) |
8 |
5 7
|
mpbird |
|- ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) ) |