Theorem pwfin0

Description: A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	pwfin0	$$⊢𝒫A\cap \mathrm{Fin}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0pwfi	$$⊢\varnothing \in \left(𝒫A\cap \mathrm{Fin}\right)$$
2		ne0i	$$⊢\varnothing \in \left(𝒫A\cap \mathrm{Fin}\right)\to 𝒫A\cap \mathrm{Fin}\ne \varnothing$$
3	1 2	ax-mp	$$⊢𝒫A\cap \mathrm{Fin}\ne \varnothing$$