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 AFinIaAFinII

Proof

Step Hyp Ref Expression
1 elpwi b𝒫AbA
2 fin1ai AFinIabAbFinAbFin
3 fin12 AbFinAbFinII
4 3 orim2i bFinAbFinbFinAbFinII
5 2 4 syl AFinIabAbFinAbFinII
6 1 5 sylan2 AFinIab𝒫AbFinAbFinII
7 6 ralrimiva AFinIab𝒫AbFinAbFinII
8 fin1a2s AFinIab𝒫AbFinAbFinIIAFinII
9 7 8 mpdan AFinIaAFinII