Description: A set is V-finite iff it behaves finitely under |_| . Definition V of Levy58 p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | df-fin5 | |- Fin5 = { x | ( x = (/) \/ x ~< ( x |_| x ) ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cfin5 | |- Fin5 |
|
1 | vx | |- x |
|
2 | 1 | cv | |- x |
3 | c0 | |- (/) |
|
4 | 2 3 | wceq | |- x = (/) |
5 | csdm | |- ~< |
|
6 | 2 2 | cdju | |- ( x |_| x ) |
7 | 2 6 5 | wbr | |- x ~< ( x |_| x ) |
8 | 4 7 | wo | |- ( x = (/) \/ x ~< ( x |_| x ) ) |
9 | 8 1 | cab | |- { x | ( x = (/) \/ x ~< ( x |_| x ) ) } |
10 | 0 9 | wceq | |- Fin5 = { x | ( x = (/) \/ x ~< ( x |_| x ) ) } |