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=\left\{y\in \left({2_{𝑜}}^A\right)|{finSupp}_{\varnothing }\left(y\right)\right\}$$
Assertion	pwfi2en	$$⊢A\in V\to S\approx \left(𝒫A\cap \mathrm{Fin}\right)$$

Proof

Step	Hyp	Ref	Expression
1		pwfi2en.s	$$⊢S=\left\{y\in \left({2_{𝑜}}^A\right)|{finSupp}_{\varnothing }\left(y\right)\right\}$$
2		eqid	$$⊢\left(x\in S⟼x^{-1}\left[\left\{1_{𝑜}\right\}\right]\right)=\left(x\in S⟼x^{-1}\left[\left\{1_{𝑜}\right\}\right]\right)$$
3	1 2	pwfi2f1o	$$⊢A\in V\to \left(x\in S⟼x^{-1}\left[\left\{1_{𝑜}\right\}\right]\right):S\underset{1-1\; onto}{⟶}𝒫A\cap \mathrm{Fin}$$
4		ovex	$$⊢{2_{𝑜}}^A\in \mathrm{V}$$
5	1 4	rabex2	$$⊢S\in \mathrm{V}$$
6	5	f1oen	$$⊢\left(x\in S⟼x^{-1}\left[\left\{1_{𝑜}\right\}\right]\right):S\underset{1-1\; onto}{⟶}𝒫A\cap \mathrm{Fin}\to S\approx \left(𝒫A\cap \mathrm{Fin}\right)$$
7	3 6	syl	$$⊢A\in V\to S\approx \left(𝒫A\cap \mathrm{Fin}\right)$$