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 ) ) |