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 e. ( _V \ Fin ) <-> ~P A e. ( _V \ Fin ) )

Proof

Step Hyp Ref Expression
1 vuniex 
 |-  U. x e. _V
2 vpwex 
 |-  ~P x e. _V
3 1 2 pm3.2i 
 |-  ( U. x e. _V /\ ~P x e. _V )
4 3 rgenw 
 |-  A. x e. _V ( U. x e. _V /\ ~P x e. _V )
5 pwinfig 
 |-  ( A. x e. _V ( U. x e. _V /\ ~P x e. _V ) -> ( A e. ( _V \ Fin ) <-> ~P A e. ( _V \ Fin ) ) )
6 4 5 ax-mp 
 |-  ( A e. ( _V \ Fin ) <-> ~P A e. ( _V \ Fin ) )