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) Avoid ax-pow . (Revised by BTernaryTau, 7-Sep-2024)

Ref Expression
Assertion pwfi ⊢ A ∈ Fin ↔ 𝒫 A ∈ Fin

Proof

Step Hyp Ref Expression
1 pweq ⊢ x = ∅ → 𝒫 x = 𝒫 ∅
2 1 eleq1d ⊢ x = ∅ → 𝒫 x ∈ Fin ↔ 𝒫 ∅ ∈ Fin
3 pweq ⊢ x = y → 𝒫 x = 𝒫 y
4 3 eleq1d ⊢ x = y → 𝒫 x ∈ Fin ↔ 𝒫 y ∈ Fin
5 pweq ⊢ x = y ∪ z → 𝒫 x = 𝒫 y ∪ z
6 5 eleq1d ⊢ x = y ∪ z → 𝒫 x ∈ Fin ↔ 𝒫 y ∪ z ∈ Fin
7 pweq ⊢ x = A → 𝒫 x = 𝒫 A
8 7 eleq1d ⊢ x = A → 𝒫 x ∈ Fin ↔ 𝒫 A ∈ Fin
9 pw0 ⊢ 𝒫 ∅ = ∅
10 snfi ⊢ ∅ ∈ Fin
11 9 10 eqeltri ⊢ 𝒫 ∅ ∈ Fin
12 eqid ⊢ c ∈ 𝒫 y ⟼ c ∪ z = c ∈ 𝒫 y ⟼ c ∪ z
13 12 pwfilem ⊢ 𝒫 y ∈ Fin → 𝒫 y ∪ z ∈ Fin
14 13 a1i ⊢ y ∈ Fin → 𝒫 y ∈ Fin → 𝒫 y ∪ z ∈ Fin
15 2 4 6 8 11 14 findcard2 ⊢ A ∈ Fin → 𝒫 A ∈ Fin
16 pwfir ⊢ 𝒫 A ∈ Fin → A ∈ Fin
17 15 16 impbii ⊢ A ∈ Fin ↔ 𝒫 A ∈ Fin