Step |
Hyp |
Ref |
Expression |
1 |
|
compss.a |
|- F = ( x e. ~P A |-> ( A \ x ) ) |
2 |
1
|
compsscnv |
|- `' F = F |
3 |
2
|
imaeq1i |
|- ( `' F " ( F " X ) ) = ( F " ( F " X ) ) |
4 |
1
|
compssiso |
|- ( A e. V -> F Isom [C.] , `' [C.] ( ~P A , ~P A ) ) |
5 |
|
isof1o |
|- ( F Isom [C.] , `' [C.] ( ~P A , ~P A ) -> F : ~P A -1-1-onto-> ~P A ) |
6 |
|
f1of1 |
|- ( F : ~P A -1-1-onto-> ~P A -> F : ~P A -1-1-> ~P A ) |
7 |
4 5 6
|
3syl |
|- ( A e. V -> F : ~P A -1-1-> ~P A ) |
8 |
|
f1imacnv |
|- ( ( F : ~P A -1-1-> ~P A /\ X C_ ~P A ) -> ( `' F " ( F " X ) ) = X ) |
9 |
7 8
|
sylan |
|- ( ( A e. V /\ X C_ ~P A ) -> ( `' F " ( F " X ) ) = X ) |
10 |
3 9
|
eqtr3id |
|- ( ( A e. V /\ X C_ ~P A ) -> ( F " ( F " X ) ) = X ) |