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	|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( A e. ( B \ Fin ) <-> ~P A e. ( B \ Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		pwelg	|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( A e. B <-> ~P A e. B ) )
2		pwfi	|- ( A e. Fin <-> ~P A e. Fin )
3	2	notbii	|- ( -. A e. Fin <-> -. ~P A e. Fin )
4	3	a1i	|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( -. A e. Fin <-> -. ~P A e. Fin ) )
5	1 4	anbi12d	|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( ( A e. B /\ -. A e. Fin ) <-> ( ~P A e. B /\ -. ~P A e. Fin ) ) )
6		eldif	|- ( A e. ( B \ Fin ) <-> ( A e. B /\ -. A e. Fin ) )
7		eldif	|- ( ~P A e. ( B \ Fin ) <-> ( ~P A e. B /\ -. ~P A e. Fin ) )
8	5 6 7	3bitr4g	|- ( A. x e. B ( U. x e. B /\ ~P x e. B ) -> ( A e. ( B \ Fin ) <-> ~P A e. ( B \ Fin ) ) )