# Metamath Proof Explorer

## Theorem pwfi

Description: The power set of a finite set is finite and vice-versa. Theorem 38 of Suppes p. 104 and its converse, Theorem 40 of Suppes p. 105. (Contributed by NM, 26-Mar-2007)

Ref Expression
Assertion pwfi ${⊢}{A}\in \mathrm{Fin}↔𝒫{A}\in \mathrm{Fin}$

### Proof

Step Hyp Ref Expression
1 isfi ${⊢}{A}\in \mathrm{Fin}↔\exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{A}\approx {m}$
2 pweq ${⊢}{m}=\varnothing \to 𝒫{m}=𝒫\varnothing$
3 2 eleq1d ${⊢}{m}=\varnothing \to \left(𝒫{m}\in \mathrm{Fin}↔𝒫\varnothing \in \mathrm{Fin}\right)$
4 pweq ${⊢}{m}={k}\to 𝒫{m}=𝒫{k}$
5 4 eleq1d ${⊢}{m}={k}\to \left(𝒫{m}\in \mathrm{Fin}↔𝒫{k}\in \mathrm{Fin}\right)$
6 pweq ${⊢}{m}=\mathrm{suc}{k}\to 𝒫{m}=𝒫\mathrm{suc}{k}$
7 df-suc ${⊢}\mathrm{suc}{k}={k}\cup \left\{{k}\right\}$
8 7 pweqi ${⊢}𝒫\mathrm{suc}{k}=𝒫\left({k}\cup \left\{{k}\right\}\right)$
9 6 8 syl6eq ${⊢}{m}=\mathrm{suc}{k}\to 𝒫{m}=𝒫\left({k}\cup \left\{{k}\right\}\right)$
10 9 eleq1d ${⊢}{m}=\mathrm{suc}{k}\to \left(𝒫{m}\in \mathrm{Fin}↔𝒫\left({k}\cup \left\{{k}\right\}\right)\in \mathrm{Fin}\right)$
11 pw0 ${⊢}𝒫\varnothing =\left\{\varnothing \right\}$
12 df1o2 ${⊢}{1}_{𝑜}=\left\{\varnothing \right\}$
13 11 12 eqtr4i ${⊢}𝒫\varnothing ={1}_{𝑜}$
14 1onn ${⊢}{1}_{𝑜}\in \mathrm{\omega }$
15 ssid ${⊢}{1}_{𝑜}\subseteq {1}_{𝑜}$
16 ssnnfi ${⊢}\left({1}_{𝑜}\in \mathrm{\omega }\wedge {1}_{𝑜}\subseteq {1}_{𝑜}\right)\to {1}_{𝑜}\in \mathrm{Fin}$
17 14 15 16 mp2an ${⊢}{1}_{𝑜}\in \mathrm{Fin}$
18 13 17 eqeltri ${⊢}𝒫\varnothing \in \mathrm{Fin}$
19 eqid ${⊢}\left({c}\in 𝒫{k}⟼{c}\cup \left\{{k}\right\}\right)=\left({c}\in 𝒫{k}⟼{c}\cup \left\{{k}\right\}\right)$
20 19 pwfilem ${⊢}𝒫{k}\in \mathrm{Fin}\to 𝒫\left({k}\cup \left\{{k}\right\}\right)\in \mathrm{Fin}$
21 20 a1i ${⊢}{k}\in \mathrm{\omega }\to \left(𝒫{k}\in \mathrm{Fin}\to 𝒫\left({k}\cup \left\{{k}\right\}\right)\in \mathrm{Fin}\right)$
22 3 5 10 18 21 finds1 ${⊢}{m}\in \mathrm{\omega }\to 𝒫{m}\in \mathrm{Fin}$
23 pwen ${⊢}{A}\approx {m}\to 𝒫{A}\approx 𝒫{m}$
24 enfii ${⊢}\left(𝒫{m}\in \mathrm{Fin}\wedge 𝒫{A}\approx 𝒫{m}\right)\to 𝒫{A}\in \mathrm{Fin}$
25 22 23 24 syl2an ${⊢}\left({m}\in \mathrm{\omega }\wedge {A}\approx {m}\right)\to 𝒫{A}\in \mathrm{Fin}$
26 25 rexlimiva ${⊢}\exists {m}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{A}\approx {m}\to 𝒫{A}\in \mathrm{Fin}$
27 1 26 sylbi ${⊢}{A}\in \mathrm{Fin}\to 𝒫{A}\in \mathrm{Fin}$
28 pwexr ${⊢}𝒫{A}\in \mathrm{Fin}\to {A}\in \mathrm{V}$
29 canth2g ${⊢}{A}\in \mathrm{V}\to {A}\prec 𝒫{A}$
30 sdomdom ${⊢}{A}\prec 𝒫{A}\to {A}\preccurlyeq 𝒫{A}$
31 28 29 30 3syl ${⊢}𝒫{A}\in \mathrm{Fin}\to {A}\preccurlyeq 𝒫{A}$
32 domfi ${⊢}\left(𝒫{A}\in \mathrm{Fin}\wedge {A}\preccurlyeq 𝒫{A}\right)\to {A}\in \mathrm{Fin}$
33 31 32 mpdan ${⊢}𝒫{A}\in \mathrm{Fin}\to {A}\in \mathrm{Fin}$
34 27 33 impbii ${⊢}{A}\in \mathrm{Fin}↔𝒫{A}\in \mathrm{Fin}$