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

Metamath Proof Explorer

Theorem fin1a2

Description: Every Ia-finite set is II-finite. Theorem 1 of Levy58, p. 3. (Contributed by Stefan O'Rear, 8-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin1a2 
|- ( A e. Fin1a -> A e. Fin2 )

Proof

Step Hyp Ref Expression
1 elpwi 
 |-  ( b e. ~P A -> b C_ A )
2 fin1ai 
 |-  ( ( A e. Fin1a /\ b C_ A ) -> ( b e. Fin \/ ( A \ b ) e. Fin ) )
3 fin12 
 |-  ( ( A \ b ) e. Fin -> ( A \ b ) e. Fin2 )
4 3 orim2i 
 |-  ( ( b e. Fin \/ ( A \ b ) e. Fin ) -> ( b e. Fin \/ ( A \ b ) e. Fin2 ) )
5 2 4 syl 
 |-  ( ( A e. Fin1a /\ b C_ A ) -> ( b e. Fin \/ ( A \ b ) e. Fin2 ) )
6 1 5 sylan2 
 |-  ( ( A e. Fin1a /\ b e. ~P A ) -> ( b e. Fin \/ ( A \ b ) e. Fin2 ) )
7 6 ralrimiva 
 |-  ( A e. Fin1a -> A. b e. ~P A ( b e. Fin \/ ( A \ b ) e. Fin2 ) )
8 fin1a2s 
 |-  ( ( A e. Fin1a /\ A. b e. ~P A ( b e. Fin \/ ( A \ b ) e. Fin2 ) ) -> A e. Fin2 )
9 7 8 mpdan 
 |-  ( A e. Fin1a -> A e. Fin2 )