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