Definition df-fin6

Description: A set is VI-finite iff it behaves finitely under X. . Definition VI of Levy58 p. 4. (Contributed by Stefan O'Rear, 12-Nov-2014)

	Ref	Expression
Assertion	df-fin6	$$⊢{\mathrm{Fin}}^{\mathrm{VI}}=\left\{x|\left(x\prec 2_{𝑜}\vee x\prec \left(x\times x\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin6	$$class{\mathrm{Fin}}^{\mathrm{VI}}$$
1		vx	$$setvarx$$
2	1	cv	$$setvarx$$
3		csdm	$$class\prec$$
4		c2o	$$class{2}_{𝑜}$$
5	2 4 3	wbr	$$wffx\prec 2_{𝑜}$$
6	2 2	cxp	$$class\left(x\times x\right)$$
7	2 6 3	wbr	$$wffx\prec \left(x\times x\right)$$
8	5 7	wo	$$wff\left(x\prec 2_{𝑜}\vee x\prec \left(x\times x\right)\right)$$
9	8 1	cab	$$class\left\{x|\left(x\prec 2_{𝑜}\vee x\prec \left(x\times x\right)\right)\right\}$$
10	0 9	wceq	$$wff{\mathrm{Fin}}^{\mathrm{VI}}=\left\{x|\left(x\prec 2_{𝑜}\vee x\prec \left(x\times x\right)\right)\right\}$$