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	⊢ ( 𝐴 ∈ ( V ∖ Fin ) ↔ 𝒫 𝐴 ∈ ( V ∖ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		vuniex	⊢ ∪ 𝑥 ∈ V
2		vpwex	⊢ 𝒫 𝑥 ∈ V
3	1 2	pm3.2i	⊢ ( ∪ 𝑥 ∈ V ∧ 𝒫 𝑥 ∈ V )
4	3	rgenw	⊢ ∀ 𝑥 ∈ V ( ∪ 𝑥 ∈ V ∧ 𝒫 𝑥 ∈ V )
5		pwinfig	⊢ ( ∀ 𝑥 ∈ V ( ∪ 𝑥 ∈ V ∧ 𝒫 𝑥 ∈ V ) → ( 𝐴 ∈ ( V ∖ Fin ) ↔ 𝒫 𝐴 ∈ ( V ∖ Fin ) ) )
6	4 5	ax-mp	⊢ ( 𝐴 ∈ ( V ∖ Fin ) ↔ 𝒫 𝐴 ∈ ( V ∖ Fin ) )