pwssfi

Description: Every element of the power set of A is finite if and only if A is finite. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	pwssfi	$⊢ A \in V \to (A \in Fin \leftrightarrow 𝒫 A \subseteq Fin)$

Step	Hyp	Ref	Expression
1		elpwi	$⊢ x \in 𝒫 A \to x \subseteq A$
2		ssfi	$⊢ (A \in Fin \land x \subseteq A) \to x \in Fin$
3	1 2	sylan2	$⊢ (A \in Fin \land x \in 𝒫 A) \to x \in Fin$
4	3	ralrimiva	$⊢ A \in Fin \to \forall x \in 𝒫 A x \in Fin$
5		dfss3	$⊢ 𝒫 A \subseteq Fin \leftrightarrow \forall x \in 𝒫 A x \in Fin$
6	4 5	sylibr	$⊢ A \in Fin \to 𝒫 A \subseteq Fin$
7		pwidg	$⊢ A \in V \to A \in 𝒫 A$
8	5	biimpi	$⊢ 𝒫 A \subseteq Fin \to \forall x \in 𝒫 A x \in Fin$
9		eleq1	$⊢ x = A \to (x \in Fin \leftrightarrow A \in Fin)$
10	9	rspcva	$⊢ (A \in 𝒫 A \land \forall x \in 𝒫 A x \in Fin) \to A \in Fin$
11	7 8 10	syl2an	$⊢ (A \in V \land 𝒫 A \subseteq Fin) \to A \in Fin$
12	11	ex	$⊢ A \in V \to (𝒫 A \subseteq Fin \to A \in Fin)$
13	6 12	impbid2	$⊢ A \in V \to (A \in Fin \leftrightarrow 𝒫 A \subseteq Fin)$

Metamath Proof Explorer