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 )