Theorem ackbij1lem10

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	ackbij1lem10	|- F : ( ~P _om i^i Fin ) --> _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		elinel2	|- ( x e. ( ~P _om i^i Fin ) -> x e. Fin )
3		snfi	|- { y } e. Fin
4		elinel1	|- ( x e. ( ~P _om i^i Fin ) -> x e. ~P _om )
5	4	elpwid	|- ( x e. ( ~P _om i^i Fin ) -> x C_ _om )
6		onfin2	|- _om = ( On i^i Fin )
7		inss2	|- ( On i^i Fin ) C_ Fin
8	6 7	eqsstri	|- _om C_ Fin
9	5 8	sstrdi	|- ( x e. ( ~P _om i^i Fin ) -> x C_ Fin )
10	9	sselda	|- ( ( x e. ( ~P _om i^i Fin ) /\ y e. x ) -> y e. Fin )
11		pwfi	|- ( y e. Fin <-> ~P y e. Fin )
12	10 11	sylib	|- ( ( x e. ( ~P _om i^i Fin ) /\ y e. x ) -> ~P y e. Fin )
13		xpfi	|- ( ( { y } e. Fin /\ ~P y e. Fin ) -> ( { y } X. ~P y ) e. Fin )
14	3 12 13	sylancr	|- ( ( x e. ( ~P _om i^i Fin ) /\ y e. x ) -> ( { y } X. ~P y ) e. Fin )
15	14	ralrimiva	|- ( x e. ( ~P _om i^i Fin ) -> A. y e. x ( { y } X. ~P y ) e. Fin )
16		iunfi	|- ( ( x e. Fin /\ A. y e. x ( { y } X. ~P y ) e. Fin ) -> U_ y e. x ( { y } X. ~P y ) e. Fin )
17	2 15 16	syl2anc	|- ( x e. ( ~P _om i^i Fin ) -> U_ y e. x ( { y } X. ~P y ) e. Fin )
18		ficardom	|- ( U_ y e. x ( { y } X. ~P y ) e. Fin -> ( card ` U_ y e. x ( { y } X. ~P y ) ) e. _om )
19	17 18	syl	|- ( x e. ( ~P _om i^i Fin ) -> ( card ` U_ y e. x ( { y } X. ~P y ) ) e. _om )
20	1 19	fmpti	|- F : ( ~P _om i^i Fin ) --> _om