Step |
Hyp |
Ref |
Expression |
1 |
|
pclfval.a |
|- A = ( Atoms ` K ) |
2 |
|
pclfval.s |
|- S = ( PSubSp ` K ) |
3 |
|
pclfval.c |
|- U = ( PCl ` K ) |
4 |
|
elex |
|- ( K e. V -> K e. _V ) |
5 |
|
fveq2 |
|- ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) ) |
6 |
5 1
|
eqtr4di |
|- ( k = K -> ( Atoms ` k ) = A ) |
7 |
6
|
pweqd |
|- ( k = K -> ~P ( Atoms ` k ) = ~P A ) |
8 |
|
fveq2 |
|- ( k = K -> ( PSubSp ` k ) = ( PSubSp ` K ) ) |
9 |
8 2
|
eqtr4di |
|- ( k = K -> ( PSubSp ` k ) = S ) |
10 |
9
|
rabeqdv |
|- ( k = K -> { y e. ( PSubSp ` k ) | x C_ y } = { y e. S | x C_ y } ) |
11 |
10
|
inteqd |
|- ( k = K -> |^| { y e. ( PSubSp ` k ) | x C_ y } = |^| { y e. S | x C_ y } ) |
12 |
7 11
|
mpteq12dv |
|- ( k = K -> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) ) |
13 |
|
df-pclN |
|- PCl = ( k e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) ) |
14 |
1
|
fvexi |
|- A e. _V |
15 |
14
|
pwex |
|- ~P A e. _V |
16 |
15
|
mptex |
|- ( x e. ~P A |-> |^| { y e. S | x C_ y } ) e. _V |
17 |
12 13 16
|
fvmpt |
|- ( K e. _V -> ( PCl ` K ) = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) ) |
18 |
3 17
|
eqtrid |
|- ( K e. _V -> U = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) ) |
19 |
4 18
|
syl |
|- ( K e. V -> U = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) ) |