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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpwi | |
|
2 | fin1ai | |
|
3 | fin12 | |
|
4 | 3 | orim2i | |
5 | 2 4 | syl | |
6 | 1 5 | sylan2 | |
7 | 6 | ralrimiva | |
8 | fin1a2s | |
|
9 | 7 8 | mpdan | |