Theorem pwfi2en

Description: Finitely supported indicator functions are equinumerous to finite subsets.MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015) (Revised by AV, 14-Jun-2020)

	Ref	Expression
Hypothesis	pwfi2en.s	|- S = { y e. ( 2o ^m A ) | y finSupp (/) }
Assertion	pwfi2en	|- ( A e. V -> S ~~ ( ~P A i^i Fin ) )

Proof

Step	Hyp	Ref	Expression
1		pwfi2en.s	|- S = { y e. ( 2o ^m A ) | y finSupp (/) }
2		eqid	|- ( x e. S |-> ( `' x " { 1o } ) ) = ( x e. S |-> ( `' x " { 1o } ) )
3	1 2	pwfi2f1o	|- ( A e. V -> ( x e. S |-> ( `' x " { 1o } ) ) : S -1-1-onto-> ( ~P A i^i Fin ) )
4		ovex	|- ( 2o ^m A ) e. _V
5	1 4	rabex2	|- S e. _V
6	5	f1oen	|- ( ( x e. S |-> ( `' x " { 1o } ) ) : S -1-1-onto-> ( ~P A i^i Fin ) -> S ~~ ( ~P A i^i Fin ) )
7	3 6	syl	|- ( A e. V -> S ~~ ( ~P A i^i Fin ) )