Metamath Proof Explorer

Theorem pwinfig

Description: The powerclass of an infinite set is an infinite set, and vice-versa. Here B is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020)

		Ref	Expression
	Assertion	pwinfig	$⊢ \forall x \in B (⋃ x \in B \land 𝒫 x \in B) \to (A \in (B ∖ Fin) \leftrightarrow 𝒫 A \in (B ∖ Fin))$

Proof

Step	Hyp	Ref	Expression
1		pwelg	$⊢ \forall x \in B (⋃ x \in B \land 𝒫 x \in B) \to (A \in B \leftrightarrow 𝒫 A \in B)$
2		pwfi	$⊢ A \in Fin \leftrightarrow 𝒫 A \in Fin$
3	2	notbii	$⊢ \neg A \in Fin \leftrightarrow \neg 𝒫 A \in Fin$
4	3	a1i	$⊢ \forall x \in B (⋃ x \in B \land 𝒫 x \in B) \to (\neg A \in Fin \leftrightarrow \neg 𝒫 A \in Fin)$
5	1 4	anbi12d	$⊢ \forall x \in B (⋃ x \in B \land 𝒫 x \in B) \to ((A \in B \land \neg A \in Fin) \leftrightarrow (𝒫 A \in B \land \neg 𝒫 A \in Fin))$
6		eldif	$⊢ A \in (B ∖ Fin) \leftrightarrow (A \in B \land \neg A \in Fin)$
7		eldif	$⊢ 𝒫 A \in (B ∖ Fin) \leftrightarrow (𝒫 A \in B \land \neg 𝒫 A \in Fin)$
8	5 6 7	3bitr4g	$⊢ \forall x \in B (⋃ x \in B \land 𝒫 x \in B) \to (A \in (B ∖ Fin) \leftrightarrow 𝒫 A \in (B ∖ Fin))$