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

Proof

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