Metamath Proof Explorer

Theorem 0pwfi

Description: The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion 0pwfi 
|- (/) e. ( ~P A i^i Fin )

Proof

Step Hyp Ref Expression
1 0elpw 
 |-  (/) e. ~P A
2 0fin 
 |-  (/) e. Fin
3 1 2 elini 
 |-  (/) e. ( ~P A i^i Fin )