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		simpl	|- ( ( A e. Fin /\ x e. ~P A ) -> A e. Fin )
2		elpwi	|- ( x e. ~P A -> x C_ A )
3	2	adantl	|- ( ( A e. Fin /\ x e. ~P A ) -> x C_ A )
4		ssfi	|- ( ( A e. Fin /\ x C_ A ) -> x e. Fin )
5	1 3 4	syl2anc	|- ( ( A e. Fin /\ x e. ~P A ) -> x e. Fin )
6	5	ralrimiva	|- ( A e. Fin -> A. x e. ~P A x e. Fin )
7		dfss3	|- ( ~P A C_ Fin <-> A. x e. ~P A x e. Fin )
8	6 7	sylibr	|- ( A e. Fin -> ~P A C_ Fin )
9	8	a1i	|- ( A e. V -> ( A e. Fin -> ~P A C_ Fin ) )
10		pwidg	|- ( A e. V -> A e. ~P A )
11	10	adantr	|- ( ( A e. V /\ ~P A C_ Fin ) -> A e. ~P A )
12	7	biimpi	|- ( ~P A C_ Fin -> A. x e. ~P A x e. Fin )
13	12	adantl	|- ( ( A e. V /\ ~P A C_ Fin ) -> A. x e. ~P A x e. Fin )
14		eleq1	|- ( x = A -> ( x e. Fin <-> A e. Fin ) )
15	14	rspcva	|- ( ( A e. ~P A /\ A. x e. ~P A x e. Fin ) -> A e. Fin )
16	11 13 15	syl2anc	|- ( ( A e. V /\ ~P A C_ Fin ) -> A e. Fin )
17	16	ex	|- ( A e. V -> ( ~P A C_ Fin -> A e. Fin ) )
18	9 17	impbid	|- ( A e. V -> ( A e. Fin <-> ~P A C_ Fin ) )