# 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}\in {\mathrm{Fin}}^{Ia}\to {A}\in {\mathrm{Fin}}^{II}$

### Proof

Step Hyp Ref Expression
1 elpwi ${⊢}{b}\in 𝒫{A}\to {b}\subseteq {A}$
2 fin1ai ${⊢}\left({A}\in {\mathrm{Fin}}^{Ia}\wedge {b}\subseteq {A}\right)\to \left({b}\in \mathrm{Fin}\vee {A}\setminus {b}\in \mathrm{Fin}\right)$
3 fin12 ${⊢}{A}\setminus {b}\in \mathrm{Fin}\to {A}\setminus {b}\in {\mathrm{Fin}}^{II}$
4 3 orim2i ${⊢}\left({b}\in \mathrm{Fin}\vee {A}\setminus {b}\in \mathrm{Fin}\right)\to \left({b}\in \mathrm{Fin}\vee {A}\setminus {b}\in {\mathrm{Fin}}^{II}\right)$
5 2 4 syl ${⊢}\left({A}\in {\mathrm{Fin}}^{Ia}\wedge {b}\subseteq {A}\right)\to \left({b}\in \mathrm{Fin}\vee {A}\setminus {b}\in {\mathrm{Fin}}^{II}\right)$
6 1 5 sylan2 ${⊢}\left({A}\in {\mathrm{Fin}}^{Ia}\wedge {b}\in 𝒫{A}\right)\to \left({b}\in \mathrm{Fin}\vee {A}\setminus {b}\in {\mathrm{Fin}}^{II}\right)$
7 6 ralrimiva ${⊢}{A}\in {\mathrm{Fin}}^{Ia}\to \forall {b}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({b}\in \mathrm{Fin}\vee {A}\setminus {b}\in {\mathrm{Fin}}^{II}\right)$
8 fin1a2s ${⊢}\left({A}\in {\mathrm{Fin}}^{Ia}\wedge \forall {b}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({b}\in \mathrm{Fin}\vee {A}\setminus {b}\in {\mathrm{Fin}}^{II}\right)\right)\to {A}\in {\mathrm{Fin}}^{II}$
9 7 8 mpdan ${⊢}{A}\in {\mathrm{Fin}}^{Ia}\to {A}\in {\mathrm{Fin}}^{II}$