Definition df-fin7 9113

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.)

Assertion

Ref	Expression
df-fin7	|- FinVII = { x | -. E. y e. ( On \ om ) x ~~ y }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-fin7

Step	Hyp	Ref	Expression
1		cfin7 9106	. 2 class FinVII
2		vx	. . . . . . 7 setvar x
3	2	cv 1482	. . . . . 6 class x
4		vy	. . . . . . 7 setvar y
5	4	cv 1482	. . . . . 6 class y
6		cen 7952	. . . . . 6 class ~~
7	3, 5, 6	wbr 4653	. . . . 5 wff x ~~ y
8		con0 5723	. . . . . 6 class On
9		com 7065	. . . . . 6 class om
10	8, 9	cdif 3571	. . . . 5 class ( On \ om )
11	7, 4, 10	wrex 2913	. . . 4 wff E. y e. ( On \ om ) x ~~ y
12	11	wn 3	. . 3 wff -. E. y e. ( On \ om ) x ~~ y
13	12, 2	cab 2608	. 2 class { x | -. E. y e. ( On \ om ) x ~~ y }
14	1, 13	wceq 1483	1 wff FinVII = { x | -. E. y e. ( On \ om ) x ~~ y }

This definition is referenced by:  isfin7  9123