| 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 |
1
|
ackbij1lem10 |
|- F : ( ~P _om i^i Fin ) --> _om |
| 3 |
1
|
ackbij1lem16 |
|- ( ( a e. ( ~P _om i^i Fin ) /\ b e. ( ~P _om i^i Fin ) ) -> ( ( F ` a ) = ( F ` b ) -> a = b ) ) |
| 4 |
3
|
rgen2 |
|- A. a e. ( ~P _om i^i Fin ) A. b e. ( ~P _om i^i Fin ) ( ( F ` a ) = ( F ` b ) -> a = b ) |
| 5 |
|
dff13 |
|- ( F : ( ~P _om i^i Fin ) -1-1-> _om <-> ( F : ( ~P _om i^i Fin ) --> _om /\ A. a e. ( ~P _om i^i Fin ) A. b e. ( ~P _om i^i Fin ) ( ( F ` a ) = ( F ` b ) -> a = b ) ) ) |
| 6 |
2 4 5
|
mpbir2an |
|- F : ( ~P _om i^i Fin ) -1-1-> _om |