| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ackbij.f |
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) ) |
| 2 |
|
sneq |
|- ( a = A -> { a } = { A } ) |
| 3 |
2
|
fveq2d |
|- ( a = A -> ( F ` { a } ) = ( F ` { A } ) ) |
| 4 |
|
pweq |
|- ( a = A -> ~P a = ~P A ) |
| 5 |
4
|
fveq2d |
|- ( a = A -> ( card ` ~P a ) = ( card ` ~P A ) ) |
| 6 |
3 5
|
eqeq12d |
|- ( a = A -> ( ( F ` { a } ) = ( card ` ~P a ) <-> ( F ` { A } ) = ( card ` ~P A ) ) ) |
| 7 |
|
ackbij1lem4 |
|- ( a e. _om -> { a } e. ( ~P _om i^i Fin ) ) |
| 8 |
1
|
ackbij1lem7 |
|- ( { a } e. ( ~P _om i^i Fin ) -> ( F ` { a } ) = ( card ` U_ y e. { a } ( { y } X. ~P y ) ) ) |
| 9 |
7 8
|
syl |
|- ( a e. _om -> ( F ` { a } ) = ( card ` U_ y e. { a } ( { y } X. ~P y ) ) ) |
| 10 |
|
vex |
|- a e. _V |
| 11 |
|
sneq |
|- ( y = a -> { y } = { a } ) |
| 12 |
|
pweq |
|- ( y = a -> ~P y = ~P a ) |
| 13 |
11 12
|
xpeq12d |
|- ( y = a -> ( { y } X. ~P y ) = ( { a } X. ~P a ) ) |
| 14 |
10 13
|
iunxsn |
|- U_ y e. { a } ( { y } X. ~P y ) = ( { a } X. ~P a ) |
| 15 |
14
|
fveq2i |
|- ( card ` U_ y e. { a } ( { y } X. ~P y ) ) = ( card ` ( { a } X. ~P a ) ) |
| 16 |
|
vpwex |
|- ~P a e. _V |
| 17 |
|
xpsnen2g |
|- ( ( a e. _V /\ ~P a e. _V ) -> ( { a } X. ~P a ) ~~ ~P a ) |
| 18 |
10 16 17
|
mp2an |
|- ( { a } X. ~P a ) ~~ ~P a |
| 19 |
|
carden2b |
|- ( ( { a } X. ~P a ) ~~ ~P a -> ( card ` ( { a } X. ~P a ) ) = ( card ` ~P a ) ) |
| 20 |
18 19
|
ax-mp |
|- ( card ` ( { a } X. ~P a ) ) = ( card ` ~P a ) |
| 21 |
15 20
|
eqtri |
|- ( card ` U_ y e. { a } ( { y } X. ~P y ) ) = ( card ` ~P a ) |
| 22 |
9 21
|
eqtrdi |
|- ( a e. _om -> ( F ` { a } ) = ( card ` ~P a ) ) |
| 23 |
6 22
|
vtoclga |
|- ( A e. _om -> ( F ` { A } ) = ( card ` ~P A ) ) |