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