Theorem ackbij1lem8

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 19-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	ackbij1lem8	|- ( A e. _om -> ( F ` { A } ) = ( card ` ~P A ) )

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