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