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	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) → ( 𝐴 ∈ ( 𝑇 ∖ Fin ) ↔ 𝒫 𝐴 ∈ ( 𝑇 ∖ Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		tskuni	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝑥 ∈ 𝑇 ) → ∪ 𝑥 ∈ 𝑇 )
2	1	3expia	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) → ( 𝑥 ∈ 𝑇 → ∪ 𝑥 ∈ 𝑇 ) )
3		tskpw	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ) → 𝒫 𝑥 ∈ 𝑇 )
4	3	ex	⊢ ( 𝑇 ∈ Tarski → ( 𝑥 ∈ 𝑇 → 𝒫 𝑥 ∈ 𝑇 ) )
5	4	adantr	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) → ( 𝑥 ∈ 𝑇 → 𝒫 𝑥 ∈ 𝑇 ) )
6	2 5	jcad	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) → ( 𝑥 ∈ 𝑇 → ( ∪ 𝑥 ∈ 𝑇 ∧ 𝒫 𝑥 ∈ 𝑇 ) ) )
7	6	ralrimiv	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) → ∀ 𝑥 ∈ 𝑇 ( ∪ 𝑥 ∈ 𝑇 ∧ 𝒫 𝑥 ∈ 𝑇 ) )
8		pwinfig	⊢ ( ∀ 𝑥 ∈ 𝑇 ( ∪ 𝑥 ∈ 𝑇 ∧ 𝒫 𝑥 ∈ 𝑇 ) → ( 𝐴 ∈ ( 𝑇 ∖ Fin ) ↔ 𝒫 𝐴 ∈ ( 𝑇 ∖ Fin ) ) )
9	7 8	syl	⊢ ( ( 𝑇 ∈ Tarski ∧ Tr 𝑇 ) → ( 𝐴 ∈ ( 𝑇 ∖ Fin ) ↔ 𝒫 𝐴 ∈ ( 𝑇 ∖ Fin ) ) )