Theorem pwfin0

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

	Ref	Expression
Assertion	pwfin0	⊢ ( 𝒫 𝐴 ∩ Fin ) ≠ ∅

Proof

Step	Hyp	Ref	Expression
1		0pwfi	⊢ ∅ ∈ ( 𝒫 𝐴 ∩ Fin )
2		ne0i	⊢ ( ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) → ( 𝒫 𝐴 ∩ Fin ) ≠ ∅ )
3	1 2	ax-mp	⊢ ( 𝒫 𝐴 ∩ Fin ) ≠ ∅