Theorem ackbij1lem7

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 21-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	ackbij1lem7	|- ( A e. ( ~P _om i^i Fin ) -> ( F ` A ) = ( card ` U_ y e. A ( { y } X. ~P y ) ) )

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		iuneq1	|- ( x = A -> U_ y e. x ( { y } X. ~P y ) = U_ y e. A ( { y } X. ~P y ) )
3	2	fveq2d	|- ( x = A -> ( card ` U_ y e. x ( { y } X. ~P y ) ) = ( card ` U_ y e. A ( { y } X. ~P y ) ) )
4		fvex	|- ( card ` U_ y e. A ( { y } X. ~P y ) ) e. _V
5	3 1 4	fvmpt	|- ( A e. ( ~P _om i^i Fin ) -> ( F ` A ) = ( card ` U_ y e. A ( { y } X. ~P y ) ) )