Theorem pwssfi

Description: Every element of the power set of A is finite if and only if A is finite. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	pwssfi	|- ( A e. V -> ( A e. Fin <-> ~P A C_ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		elpwi	|- ( x e. ~P A -> x C_ A )
2		ssfi	|- ( ( A e. Fin /\ x C_ A ) -> x e. Fin )
3	1 2	sylan2	|- ( ( A e. Fin /\ x e. ~P A ) -> x e. Fin )
4	3	ralrimiva	|- ( A e. Fin -> A. x e. ~P A x e. Fin )
5		dfss3	|- ( ~P A C_ Fin <-> A. x e. ~P A x e. Fin )
6	4 5	sylibr	|- ( A e. Fin -> ~P A C_ Fin )
7		pwidg	|- ( A e. V -> A e. ~P A )
8	5	biimpi	|- ( ~P A C_ Fin -> A. x e. ~P A x e. Fin )
9		eleq1	|- ( x = A -> ( x e. Fin <-> A e. Fin ) )
10	9	rspcva	|- ( ( A e. ~P A /\ A. x e. ~P A x e. Fin ) -> A e. Fin )
11	7 8 10	syl2an	|- ( ( A e. V /\ ~P A C_ Fin ) -> A e. Fin )
12	11	ex	|- ( A e. V -> ( ~P A C_ Fin -> A e. Fin ) )
13	6 12	impbid2	|- ( A e. V -> ( A e. Fin <-> ~P A C_ Fin ) )