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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cfin7 | ||
1 | vx | ||
2 | vy | ||
3 | con0 | ||
4 | com | ||
5 | 3 4 | cdif | |
6 | 1 | cv | |
7 | cen | ||
8 | 2 | cv | |
9 | 6 8 7 | wbr | |
10 | 9 2 5 | wrex | |
11 | 10 | wn | |
12 | 11 1 | cab | |
13 | 0 12 | wceq |