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 |
1 2 3 4
|
lsatset |
|- ( W e. X -> A = ran ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) ) |
6 |
5
|
eleq2d |
|- ( W e. X -> ( U e. A <-> U e. ran ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) ) ) |
7 |
|
eqid |
|- ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) = ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) |
8 |
|
fvex |
|- ( N ` { x } ) e. _V |
9 |
7 8
|
elrnmpti |
|- ( U e. ran ( x e. ( V \ { .0. } ) |-> ( N ` { x } ) ) <-> E. x e. ( V \ { .0. } ) U = ( N ` { x } ) ) |
10 |
6 9
|
bitrdi |
|- ( W e. X -> ( U e. A <-> E. x e. ( V \ { .0. } ) U = ( N ` { x } ) ) ) |