Definition df-fin2

Description: A set is II-finite (Tarski finite) iff every nonempty chain of subsets contains a maximum element. Definition II of Levy58 p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014)

	Ref	Expression
Assertion	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\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin2	$$class{\mathrm{Fin}}^{\mathrm{II}}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4	3	cpw	$$class𝒫x$$
5	4	cpw	$$class𝒫𝒫x$$
6	2	cv	$$setvary$$
7		c0	$$class\varnothing$$
8	6 7	wne	$$wffy\ne \varnothing$$
9		crpss	$$class[\subset ]$$
10	6 9	wor	$$wff[\subset ]\mathrm{Or}y$$
11	8 10	wa	$$wff\left(y\ne \varnothing \wedge [\subset ]\mathrm{Or}y\right)$$
12	6	cuni	$$class\bigcup y$$
13	12 6	wcel	$$wff\bigcup y\in y$$
14	11 13	wi	$$wff\left(\left(y\ne \varnothing \wedge [\subset ]\mathrm{Or}y\right)\to \bigcup y\in y\right)$$
15	14 2 5	wral	$$wff\forall y\in 𝒫𝒫x\left(\left(y\ne \varnothing \wedge [\subset ]\mathrm{Or}y\right)\to \bigcup y\in y\right)$$
16	15 1	cab	$$class\left\{x|\forall y\in 𝒫𝒫x\left(\left(y\ne \varnothing \wedge [\subset ]\mathrm{Or}y\right)\to \bigcup y\in y\right)\right\}$$
17	0 16	wceq	$$wff{\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\}$$