Metamath Proof Explorer

Theorem isfin2

Description: Definition of a II-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

Ref Expression
Assertion isfin2 ${⊢}{A}\in {V}\to \left({A}\in {\mathrm{Fin}}^{II}↔\forall {y}\in 𝒫𝒫{A}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)\right)$

Proof

Step Hyp Ref Expression
1 pweq ${⊢}{z}={x}\to 𝒫{z}=𝒫{x}$
2 1 pweqd ${⊢}{z}={x}\to 𝒫𝒫{z}=𝒫𝒫{x}$
3 2 raleqdv ${⊢}{z}={x}\to \left(\forall {y}\in 𝒫𝒫{z}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)↔\forall {y}\in 𝒫𝒫{x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)\right)$
4 pweq ${⊢}{x}={A}\to 𝒫{x}=𝒫{A}$
5 4 pweqd ${⊢}{x}={A}\to 𝒫𝒫{x}=𝒫𝒫{A}$
6 5 raleqdv ${⊢}{x}={A}\to \left(\forall {y}\in 𝒫𝒫{x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)↔\forall {y}\in 𝒫𝒫{A}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)\right)$
7 df-fin2 ${⊢}{\mathrm{Fin}}^{II}=\left\{{z}|\forall {y}\in 𝒫𝒫{z}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)\right\}$
8 3 6 7 elab2gw ${⊢}{A}\in {V}\to \left({A}\in {\mathrm{Fin}}^{II}↔\forall {y}\in 𝒫𝒫{A}\phantom{\rule{.4em}{0ex}}\left(\left({y}\ne \varnothing \wedge \left[\subset \right]\mathrm{Or}{y}\right)\to \bigcup {y}\in {y}\right)\right)$