Theorem infpwfidom

Description: The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption ( ~P A i^i Fin ) e. _V because this theorem also implies that A is a set if ~P A i^i Fin is.) (Contributed by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	infpwfidom	⊢ ( ( 𝒫 𝐴 ∩ Fin ) ∈ V → 𝐴 ≼ ( 𝒫 𝐴 ∩ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		snelpwi	⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ∈ 𝒫 𝐴 )
2		snfi	⊢ { 𝑥 } ∈ Fin
3	2	a1i	⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ∈ Fin )
4	1 3	elind	⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ∈ ( 𝒫 𝐴 ∩ Fin ) )
5		sneqbg	⊢ ( 𝑥 ∈ 𝐴 → ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 ) )
6	5	adantr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 ) )
7	4 6	dom2	⊢ ( ( 𝒫 𝐴 ∩ Fin ) ∈ V → 𝐴 ≼ ( 𝒫 𝐴 ∩ Fin ) )