Theorem ackbij1lem17

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 18-Nov-2014)

	Ref	Expression
Hypothesis	ackbij.f	|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
Assertion	ackbij1lem17	|- F : ( ~P _om i^i Fin ) -1-1-> _om

Proof

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