This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )

Proof

Step Hyp Ref Expression
1 pweq ⊢ ( 𝑥 = ∅ → 𝒫 𝑥 = 𝒫 ∅ )
2 1 eleq1d ⊢ ( 𝑥 = ∅ → ( 𝒫 𝑥 ∈ Fin ↔ 𝒫 ∅ ∈ Fin ) )
3 pweq ⊢ ( 𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦 )
4 3 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝒫 𝑥 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin ) )
5 pweq ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → 𝒫 𝑥 = 𝒫 ( 𝑦 ∪ { 𝑧 } ) )
6 5 eleq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝒫 𝑥 ∈ Fin ↔ 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ) )
7 pweq ⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
8 7 eleq1d ⊢ ( 𝑥 = 𝐴 → ( 𝒫 𝑥 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin ) )
9 pw0 ⊢ 𝒫 ∅ = { ∅ }
10 snfi ⊢ { ∅ } ∈ Fin
11 9 10 eqeltri ⊢ 𝒫 ∅ ∈ Fin
12 eqid ⊢ ( 𝑐 ∈ 𝒫 𝑦 ↦ ( 𝑐 ∪ { 𝑧 } ) ) = ( 𝑐 ∈ 𝒫 𝑦 ↦ ( 𝑐 ∪ { 𝑧 } ) )
13 12 pwfilem ⊢ ( 𝒫 𝑦 ∈ Fin → 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∈ Fin )
14 13 a1i ⊢ ( 𝑦 ∈ Fin → ( 𝒫 𝑦 ∈ Fin → 𝒫 ( 𝑦 ∪ { 𝑧 } ) ∈ Fin ) )
15 2 4 6 8 11 14 findcard2 ⊢ ( 𝐴 ∈ Fin → 𝒫 𝐴 ∈ Fin )
16 pwfir ⊢ ( 𝒫 𝐴 ∈ Fin → 𝐴 ∈ Fin )
17 15 16 impbii ⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )