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 )