Metamath Proof Explorer

Theorem fin11a

Description: Every I-finite set is Ia-finite. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin11a 
|- ( A e. Fin -> A e. Fin1a )

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 orcd 
 |-  ( ( A e. Fin /\ x e. ~P A ) -> ( x e. Fin \/ ( A \ x ) e. Fin ) )
5 4 ralrimiva 
 |-  ( A e. Fin -> A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin ) )
6 isfin1a 
 |-  ( A e. Fin -> ( A e. Fin1a <-> A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin ) ) )
7 5 6 mpbird 
 |-  ( A e. Fin -> A e. Fin1a )