Theorem pwinfig

Description: The powerclass of an infinite set is an infinite set, and vice-versa. Here B is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020)

	Ref	Expression
Assertion	pwinfig	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ ( 𝐵 ∖ Fin ) ↔ 𝒫 𝐴 ∈ ( 𝐵 ∖ Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		pwelg	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ 𝐵 ↔ 𝒫 𝐴 ∈ 𝐵 ) )
2		pwfi	⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )
3	2	notbii	⊢ ( ¬ 𝐴 ∈ Fin ↔ ¬ 𝒫 𝐴 ∈ Fin )
4	3	a1i	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → ( ¬ 𝐴 ∈ Fin ↔ ¬ 𝒫 𝐴 ∈ Fin ) )
5	1 4	anbi12d	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ Fin ) ↔ ( 𝒫 𝐴 ∈ 𝐵 ∧ ¬ 𝒫 𝐴 ∈ Fin ) ) )
6		eldif	⊢ ( 𝐴 ∈ ( 𝐵 ∖ Fin ) ↔ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ Fin ) )
7		eldif	⊢ ( 𝒫 𝐴 ∈ ( 𝐵 ∖ Fin ) ↔ ( 𝒫 𝐴 ∈ 𝐵 ∧ ¬ 𝒫 𝐴 ∈ Fin ) )
8	5 6 7	3bitr4g	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵 ) → ( 𝐴 ∈ ( 𝐵 ∖ Fin ) ↔ 𝒫 𝐴 ∈ ( 𝐵 ∖ Fin ) ) )