Description: A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | pwfin0 | ⊢ ( 𝒫 𝐴 ∩ Fin ) ≠ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0pwfi | ⊢ ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) | |
2 | ne0i | ⊢ ( ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) → ( 𝒫 𝐴 ∩ Fin ) ≠ ∅ ) | |
3 | 1 2 | ax-mp | ⊢ ( 𝒫 𝐴 ∩ Fin ) ≠ ∅ |