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 ∈ Fin ↔ 𝒫 A ∈ Fin

Proof

Step Hyp Ref Expression
1 isfi ⊢ A ∈ Fin ↔ ∃ m ∈ ω A ≈ m
2 pweq ⊢ m = ∅ → 𝒫 m = 𝒫 ∅
3 2 eleq1d ⊢ m = ∅ → 𝒫 m ∈ Fin ↔ 𝒫 ∅ ∈ Fin
4 pweq ⊢ m = k → 𝒫 m = 𝒫 k
5 4 eleq1d ⊢ m = k → 𝒫 m ∈ Fin ↔ 𝒫 k ∈ Fin
6 pweq ⊢ m = suc ⁡ k → 𝒫 m = 𝒫 suc ⁡ k
7 df-suc ⊢ suc ⁡ k = k ∪ k
8 7 pweqi ⊢ 𝒫 suc ⁡ k = 𝒫 k ∪ k
9 6 8 syl6eq ⊢ m = suc ⁡ k → 𝒫 m = 𝒫 k ∪ k
10 9 eleq1d ⊢ m = suc ⁡ k → 𝒫 m ∈ Fin ↔ 𝒫 k ∪ k ∈ Fin
11 pw0 ⊢ 𝒫 ∅ = ∅
12 df1o2 ⊢ 1 𝑜 = ∅
13 11 12 eqtr4i ⊢ 𝒫 ∅ = 1 𝑜
14 1onn ⊢ 1 𝑜 ∈ ω
15 ssid ⊢ 1 𝑜 ⊆ 1 𝑜
16 ssnnfi ⊢ 1 𝑜 ∈ ω ∧ 1 𝑜 ⊆ 1 𝑜 → 1 𝑜 ∈ Fin
17 14 15 16 mp2an ⊢ 1 𝑜 ∈ Fin
18 13 17 eqeltri ⊢ 𝒫 ∅ ∈ Fin
19 eqid ⊢ c ∈ 𝒫 k ⟼ c ∪ k = c ∈ 𝒫 k ⟼ c ∪ k
20 19 pwfilem ⊢ 𝒫 k ∈ Fin → 𝒫 k ∪ k ∈ Fin
21 20 a1i ⊢ k ∈ ω → 𝒫 k ∈ Fin → 𝒫 k ∪ k ∈ Fin
22 3 5 10 18 21 finds1 ⊢ m ∈ ω → 𝒫 m ∈ Fin
23 pwen ⊢ A ≈ m → 𝒫 A ≈ 𝒫 m
24 enfii ⊢ 𝒫 m ∈ Fin ∧ 𝒫 A ≈ 𝒫 m → 𝒫 A ∈ Fin
25 22 23 24 syl2an ⊢ m ∈ ω ∧ A ≈ m → 𝒫 A ∈ Fin
26 25 rexlimiva ⊢ ∃ m ∈ ω A ≈ m → 𝒫 A ∈ Fin
27 1 26 sylbi ⊢ A ∈ Fin → 𝒫 A ∈ Fin
28 pwexr ⊢ 𝒫 A ∈ Fin → A ∈ V
29 canth2g ⊢ A ∈ V → A ≺ 𝒫 A
30 sdomdom ⊢ A ≺ 𝒫 A → A ≼ 𝒫 A
31 28 29 30 3syl ⊢ 𝒫 A ∈ Fin → A ≼ 𝒫 A
32 domfi ⊢ 𝒫 A ∈ Fin ∧ A ≼ 𝒫 A → A ∈ Fin
33 31 32 mpdan ⊢ 𝒫 A ∈ Fin → A ∈ Fin
34 27 33 impbii ⊢ A ∈ Fin ↔ 𝒫 A ∈ Fin