Definition df-fin7

Description: A set is VII-finite iff it cannot be infinitely well-ordered. Equivalent to definition VII of Levy58 p. 4. (Contributed by Stefan O'Rear, 12-Nov-2014)

	Ref	Expression
Assertion	df-fin7	$$⊢{\mathrm{Fin}}^{\mathrm{VII}}=\left\{x|\neg \exists y\in \left(\mathrm{On}\setminus \mathrm{\omega }\right)x\approx y\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin7	$$class{\mathrm{Fin}}^{\mathrm{VII}}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3		con0	$$class\mathrm{On}$$
4		com	$$class\mathrm{\omega }$$
5	3 4	cdif	$$class\left(\mathrm{On}\setminus \mathrm{\omega }\right)$$
6	1	cv	$$setvarx$$
7		cen	$$class\approx$$
8	2	cv	$$setvary$$
9	6 8 7	wbr	$$wffx\approx y$$
10	9 2 5	wrex	$$wff\exists y\in \left(\mathrm{On}\setminus \mathrm{\omega }\right)x\approx y$$
11	10	wn	$$wff\neg \exists y\in \left(\mathrm{On}\setminus \mathrm{\omega }\right)x\approx y$$
12	11 1	cab	$$class\left\{x|\neg \exists y\in \left(\mathrm{On}\setminus \mathrm{\omega }\right)x\approx y\right\}$$
13	0 12	wceq	$$wff{\mathrm{Fin}}^{\mathrm{VII}}=\left\{x|\neg \exists y\in \left(\mathrm{On}\setminus \mathrm{\omega }\right)x\approx y\right\}$$