# 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}\in \mathrm{WUni}\to \left({A}\in \left({U}\setminus \mathrm{Fin}\right)↔𝒫{A}\in \left({U}\setminus \mathrm{Fin}\right)\right)$

### Proof

Step Hyp Ref Expression
1 iswun ${⊢}{U}\in \mathrm{WUni}\to \left({U}\in \mathrm{WUni}↔\left(\mathrm{Tr}{U}\wedge {U}\ne \varnothing \wedge \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\right)\right)\right)$
2 1 ibi ${⊢}{U}\in \mathrm{WUni}\to \left(\mathrm{Tr}{U}\wedge {U}\ne \varnothing \wedge \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\right)\right)$
3 3simpa ${⊢}\left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\right)\to \left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\right)$
4 3 ralimi ${⊢}\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\right)\to \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\right)$
5 4 3ad2ant3 ${⊢}\left(\mathrm{Tr}{U}\wedge {U}\ne \varnothing \wedge \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\wedge \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {U}\right)\right)\to \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\right)$
6 pwinfig ${⊢}\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\bigcup {x}\in {U}\wedge 𝒫{x}\in {U}\right)\to \left({A}\in \left({U}\setminus \mathrm{Fin}\right)↔𝒫{A}\in \left({U}\setminus \mathrm{Fin}\right)\right)$
7 2 5 6 3syl ${⊢}{U}\in \mathrm{WUni}\to \left({A}\in \left({U}\setminus \mathrm{Fin}\right)↔𝒫{A}\in \left({U}\setminus \mathrm{Fin}\right)\right)$