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	|- Fin7 = { x | -. E. y e. ( On \ _om ) x ~~ y }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin7	|- Fin7
1		vx	|- x
2		vy	|- y
3		con0	|- On
4		com	|- _om
5	3 4	cdif	|- ( On \ _om )
6	1	cv	|- x
7		cen	|- ~~
8	2	cv	|- y
9	6 8 7	wbr	|- x ~~ y
10	9 2 5	wrex	|- E. y e. ( On \ _om ) x ~~ y
11	10	wn	|- -. E. y e. ( On \ _om ) x ~~ y
12	11 1	cab	|- { x | -. E. y e. ( On \ _om ) x ~~ y }
13	0 12	wceq	|- Fin7 = { x | -. E. y e. ( On \ _om ) x ~~ y }