Step |
Hyp |
Ref |
Expression |
1 |
|
lsatset.v |
|- V = ( Base ` W ) |
2 |
|
lsatset.n |
|- N = ( LSpan ` W ) |
3 |
|
lsatset.z |
|- .0. = ( 0g ` W ) |
4 |
|
lsatset.a |
|- A = ( LSAtoms ` W ) |
5 |
|
lsatlspsn.w |
|- ( ph -> W e. LMod ) |
6 |
|
lsatlspsn.x |
|- ( ph -> X e. ( V \ { .0. } ) ) |
7 |
|
eqid |
|- ( N ` { X } ) = ( N ` { X } ) |
8 |
|
sneq |
|- ( v = X -> { v } = { X } ) |
9 |
8
|
fveq2d |
|- ( v = X -> ( N ` { v } ) = ( N ` { X } ) ) |
10 |
9
|
rspceeqv |
|- ( ( X e. ( V \ { .0. } ) /\ ( N ` { X } ) = ( N ` { X } ) ) -> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) ) |
11 |
6 7 10
|
sylancl |
|- ( ph -> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) ) |
12 |
1 2 3 4
|
islsat |
|- ( W e. LMod -> ( ( N ` { X } ) e. A <-> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) ) ) |
13 |
5 12
|
syl |
|- ( ph -> ( ( N ` { X } ) e. A <-> E. v e. ( V \ { .0. } ) ( N ` { X } ) = ( N ` { v } ) ) ) |
14 |
11 13
|
mpbird |
|- ( ph -> ( N ` { X } ) e. A ) |