This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )