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	$$⊢𝒫A\cap \mathrm{Fin}\in \mathrm{V}\to A\preccurlyeq \left(𝒫A\cap \mathrm{Fin}\right)$$

Proof

Step	Hyp	Ref	Expression
1		snelpwi	$$⊢x\in A\to \left\{x\right\}\in 𝒫A$$
2		snfi	$$⊢\left\{x\right\}\in \mathrm{Fin}$$
3	2	a1i	$$⊢x\in A\to \left\{x\right\}\in \mathrm{Fin}$$
4	1 3	elind	$$⊢x\in A\to \left\{x\right\}\in \left(𝒫A\cap \mathrm{Fin}\right)$$
5		sneqbg	$$⊢x\in A\to \left(\left\{x\right\}=\left\{y\right\}\leftrightarrow x=y\right)$$
6	5	adantr	$$⊢\left(x\in A\wedge y\in A\right)\to \left(\left\{x\right\}=\left\{y\right\}\leftrightarrow x=y\right)$$
7	4 6	dom2	$$⊢𝒫A\cap \mathrm{Fin}\in \mathrm{V}\to A\preccurlyeq \left(𝒫A\cap \mathrm{Fin}\right)$$