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}}^{\mathrm{II}}\leftrightarrow \forall y\in 𝒫𝒫A\left(\left(y\ne \varnothing \wedge [\subset ]\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\left(\left(y\ne \varnothing \wedge [\subset ]\mathrm{Or}y\right)\to \bigcup y\in y\right)\leftrightarrow \forall y\in 𝒫𝒫x\left(\left(y\ne \varnothing \wedge [\subset ]\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\left(\left(y\ne \varnothing \wedge [\subset ]\mathrm{Or}y\right)\to \bigcup y\in y\right)\leftrightarrow \forall y\in 𝒫𝒫A\left(\left(y\ne \varnothing \wedge [\subset ]\mathrm{Or}y\right)\to \bigcup y\in y\right)\right)$$
7		df-fin2	$$⊢{\mathrm{Fin}}^{\mathrm{II}}=\left\{z|\forall y\in 𝒫𝒫z\left(\left(y\ne \varnothing \wedge [\subset ]\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}}^{\mathrm{II}}\leftrightarrow \forall y\in 𝒫𝒫A\left(\left(y\ne \varnothing \wedge [\subset ]\mathrm{Or}y\right)\to \bigcup y\in y\right)\right)$$