Metamath Proof Explorer


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 2 𝑜 A | finSupp y
Assertion pwfi2en A V S 𝒫 A Fin

Proof

Step Hyp Ref Expression
1 pwfi2en.s S = y 2 𝑜 A | finSupp y
2 eqid x S x -1 1 𝑜 = x S x -1 1 𝑜
3 1 2 pwfi2f1o A V x S x -1 1 𝑜 : S 1-1 onto 𝒫 A Fin
4 ovex 2 𝑜 A V
5 1 4 rabex2 S V
6 5 f1oen x S x -1 1 𝑜 : S 1-1 onto 𝒫 A Fin S 𝒫 A Fin
7 3 6 syl A V S 𝒫 A Fin