pwinfi2

Description: The powerclass of an infinite set is an infinite set, and vice-versa. Here U is a weak universe. (Contributed by RP, 21-Mar-2020)

		Ref	Expression
	Assertion	pwinfi2	$⊢ U \in WUni \to (A \in (U ∖ Fin) \leftrightarrow 𝒫 A \in (U ∖ Fin))$

Step	Hyp	Ref	Expression
1		iswun	$⊢ U \in WUni \to (U \in WUni \leftrightarrow (Tr U \land U \neq \emptyset \land \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U)))$
2	1	ibi	$⊢ U \in WUni \to (Tr U \land U \neq \emptyset \land \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U))$
3		3simpa	$⊢ (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U) \to (⋃ x \in U \land 𝒫 x \in U)$
4	3	ralimi	$⊢ \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U) \to \forall x \in U (⋃ x \in U \land 𝒫 x \in U)$
5	4	3ad2ant3	$⊢ (Tr U \land U \neq \emptyset \land \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U)) \to \forall x \in U (⋃ x \in U \land 𝒫 x \in U)$
6		pwinfig	$⊢ \forall x \in U (⋃ x \in U \land 𝒫 x \in U) \to (A \in (U ∖ Fin) \leftrightarrow 𝒫 A \in (U ∖ Fin))$
7	2 5 6	3syl	$⊢ U \in WUni \to (A \in (U ∖ Fin) \leftrightarrow 𝒫 A \in (U ∖ Fin))$

Metamath Proof Explorer