Theorem pwinfi3

Description: The powerclass of an infinite set is an infinite set, and vice-versa. Here T is a transitive Tarski universe. (Contributed by RP, 21-Mar-2020)

	Ref	Expression
Assertion	pwinfi3	|- ( ( T e. Tarski /\ Tr T ) -> ( A e. ( T \ Fin ) <-> ~P A e. ( T \ Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		tskuni	|- ( ( T e. Tarski /\ Tr T /\ x e. T ) -> U. x e. T )
2	1	3expia	|- ( ( T e. Tarski /\ Tr T ) -> ( x e. T -> U. x e. T ) )
3		tskpw	|- ( ( T e. Tarski /\ x e. T ) -> ~P x e. T )
4	3	ex	|- ( T e. Tarski -> ( x e. T -> ~P x e. T ) )
5	4	adantr	|- ( ( T e. Tarski /\ Tr T ) -> ( x e. T -> ~P x e. T ) )
6	2 5	jcad	|- ( ( T e. Tarski /\ Tr T ) -> ( x e. T -> ( U. x e. T /\ ~P x e. T ) ) )
7	6	ralrimiv	|- ( ( T e. Tarski /\ Tr T ) -> A. x e. T ( U. x e. T /\ ~P x e. T ) )
8		pwinfig	|- ( A. x e. T ( U. x e. T /\ ~P x e. T ) -> ( A e. ( T \ Fin ) <-> ~P A e. ( T \ Fin ) ) )
9	7 8	syl	|- ( ( T e. Tarski /\ Tr T ) -> ( A e. ( T \ Fin ) <-> ~P A e. ( T \ Fin ) ) )