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	⊢ 𝑆 = { 𝑦 ∈ ( 2o ↑m 𝐴 ) ∣ 𝑦 finSupp ∅ }
Assertion	pwfi2en	⊢ ( 𝐴 ∈ 𝑉 → 𝑆 ≈ ( 𝒫 𝐴 ∩ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		pwfi2en.s	⊢ 𝑆 = { 𝑦 ∈ ( 2o ↑m 𝐴 ) ∣ 𝑦 finSupp ∅ }
2		eqid	⊢ ( 𝑥 ∈ 𝑆 ↦ ( ◡ 𝑥 “ { 1o } ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ◡ 𝑥 “ { 1o } ) )
3	1 2	pwfi2f1o	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝑆 ↦ ( ◡ 𝑥 “ { 1o } ) ) : 𝑆 –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) )
4		ovex	⊢ ( 2o ↑m 𝐴 ) ∈ V
5	1 4	rabex2	⊢ 𝑆 ∈ V
6	5	f1oen	⊢ ( ( 𝑥 ∈ 𝑆 ↦ ( ◡ 𝑥 “ { 1o } ) ) : 𝑆 –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) → 𝑆 ≈ ( 𝒫 𝐴 ∩ Fin ) )
7	3 6	syl	⊢ ( 𝐴 ∈ 𝑉 → 𝑆 ≈ ( 𝒫 𝐴 ∩ Fin ) )