Metamath Proof Explorer

Theorem 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 ∈ WUni → A ∈ U ∖ Fin ↔ 𝒫 A ∈ U ∖ Fin

Proof

Step Hyp Ref Expression
1 iswun ⊢ U ∈ WUni → U ∈ WUni ↔ Tr ⁡ U ∧ U ≠ ∅ ∧ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
2 1 ibi ⊢ U ∈ WUni → Tr ⁡ U ∧ U ≠ ∅ ∧ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
3 3simpa ⊢ ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U → ⋃ x ∈ U ∧ 𝒫 x ∈ U
4 3 ralimi ⊢ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U → ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U
5 4 3ad2ant3 ⊢ Tr ⁡ U ∧ U ≠ ∅ ∧ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U → ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U
6 pwinfig ⊢ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U → A ∈ U ∖ Fin ↔ 𝒫 A ∈ U ∖ Fin
7 2 5 6 3syl ⊢ U ∈ WUni → A ∈ U ∖ Fin ↔ 𝒫 A ∈ U ∖ Fin