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 \in Fin \leftrightarrow 𝒫 A \in Fin$

Proof

Step	Hyp	Ref	Expression
1		pweq	$⊢ x = \emptyset \to 𝒫 x = 𝒫 \emptyset$
2	1	eleq1d	$⊢ x = \emptyset \to (𝒫 x \in Fin \leftrightarrow 𝒫 \emptyset \in Fin)$
3		pweq	$⊢ x = y \to 𝒫 x = 𝒫 y$
4	3	eleq1d	$⊢ x = y \to (𝒫 x \in Fin \leftrightarrow 𝒫 y \in Fin)$
5		pweq	$⊢ x = y \cup \{z\} \to 𝒫 x = 𝒫 (y \cup \{z\})$
6	5	eleq1d	$⊢ x = y \cup \{z\} \to (𝒫 x \in Fin \leftrightarrow 𝒫 (y \cup \{z\}) \in Fin)$
7		pweq	$⊢ x = A \to 𝒫 x = 𝒫 A$
8	7	eleq1d	$⊢ x = A \to (𝒫 x \in Fin \leftrightarrow 𝒫 A \in Fin)$
9		pw0	$⊢ 𝒫 \emptyset = \{\emptyset\}$
10		snfi	$⊢ \{\emptyset\} \in Fin$
11	9 10	eqeltri	$⊢ 𝒫 \emptyset \in Fin$
12		eqid	$⊢ (c \in 𝒫 y ⟼ c \cup \{z\}) = (c \in 𝒫 y ⟼ c \cup \{z\})$
13	12	pwfilem	$⊢ 𝒫 y \in Fin \to 𝒫 (y \cup \{z\}) \in Fin$
14	13	a1i	$⊢ y \in Fin \to (𝒫 y \in Fin \to 𝒫 (y \cup \{z\}) \in Fin)$
15	2 4 6 8 11 14	findcard2	$⊢ A \in Fin \to 𝒫 A \in Fin$
16		pwfir	$⊢ 𝒫 A \in Fin \to A \in Fin$
17	15 16	impbii	$⊢ A \in Fin \leftrightarrow 𝒫 A \in Fin$