Metamath Proof Explorer

Theorem pwinfi

Description: The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020)

Ref Expression
Assertion pwinfi ⊢ A ∈ V ∖ Fin ↔ 𝒫 A ∈ V ∖ Fin

Proof

Step Hyp Ref Expression
1 vuniex ⊢ ⋃ x ∈ V
2 vpwex ⊢ 𝒫 x ∈ V
3 1 2 pm3.2i ⊢ ⋃ x ∈ V ∧ 𝒫 x ∈ V
4 3 rgenw ⊢ ∀ x ∈ V ⋃ x ∈ V ∧ 𝒫 x ∈ V
5 pwinfig ⊢ ∀ x ∈ V ⋃ x ∈ V ∧ 𝒫 x ∈ V → A ∈ V ∖ Fin ↔ 𝒫 A ∈ V ∖ Fin
6 4 5 ax-mp ⊢ A ∈ V ∖ Fin ↔ 𝒫 A ∈ V ∖ Fin