Metamath Proof Explorer

Theorem pwinfi3

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

		Ref	Expression
	Assertion	pwinfi3	$⊢ (T \in Tarski \land Tr T) \to (A \in (T ∖ Fin) \leftrightarrow 𝒫 A \in (T ∖ Fin))$

Proof

Step	Hyp	Ref	Expression
1		tskuni	$⊢ (T \in Tarski \land Tr T \land x \in T) \to ⋃ x \in T$
2	1	3expia	$⊢ (T \in Tarski \land Tr T) \to (x \in T \to ⋃ x \in T)$
3		tskpw	$⊢ (T \in Tarski \land x \in T) \to 𝒫 x \in T$
4	3	ex	$⊢ T \in Tarski \to (x \in T \to 𝒫 x \in T)$
5	4	adantr	$⊢ (T \in Tarski \land Tr T) \to (x \in T \to 𝒫 x \in T)$
6	2 5	jcad	$⊢ (T \in Tarski \land Tr T) \to (x \in T \to (⋃ x \in T \land 𝒫 x \in T))$
7	6	ralrimiv	$⊢ (T \in Tarski \land Tr T) \to \forall x \in T (⋃ x \in T \land 𝒫 x \in T)$
8		pwinfig	$⊢ \forall x \in T (⋃ x \in T \land 𝒫 x \in T) \to (A \in (T ∖ Fin) \leftrightarrow 𝒫 A \in (T ∖ Fin))$
9	7 8	syl	$⊢ (T \in Tarski \land Tr T) \to (A \in (T ∖ Fin) \leftrightarrow 𝒫 A \in (T ∖ Fin))$