Metamath Proof Explorer


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 FinVII = x | ¬ y On ω x y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfin7 class FinVII
1 vx setvar x
2 vy setvar y
3 con0 class On
4 com class ω
5 3 4 cdif class On ω
6 1 cv setvar x
7 cen class
8 2 cv setvar y
9 6 8 7 wbr wff x y
10 9 2 5 wrex wff y On ω x y
11 10 wn wff ¬ y On ω x y
12 11 1 cab class x | ¬ y On ω x y
13 0 12 wceq wff FinVII = x | ¬ y On ω x y