Metamath Proof Explorer
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 |
|
Detailed syntax breakdown
Step |
Hyp |
Ref |
Expression |
0 |
|
cfin6 |
|
1 |
|
vx |
|
2 |
1
|
cv |
|
3 |
|
csdm |
|
4 |
|
c2o |
|
5 |
2 4 3
|
wbr |
|
6 |
2 2
|
cxp |
|
7 |
2 6 3
|
wbr |
|
8 |
5 7
|
wo |
|
9 |
8 1
|
cab |
|
10 |
0 9
|
wceq |
|