Description: A well-orderable set is VII-finite iff it is I-finite. Thus, even without choice, on the class of well-orderable sets all eight definitions of finite set coincide. (Contributed by Mario Carneiro, 18-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fin71num | |- ( A e. dom card -> ( A e. Fin7 <-> A e. Fin ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isfin7-2 | |- ( A e. dom card -> ( A e. Fin7 <-> ( A e. dom card -> A e. Fin ) ) ) |
|
2 | biimt | |- ( A e. dom card -> ( A e. Fin <-> ( A e. dom card -> A e. Fin ) ) ) |
|
3 | 1 2 | bitr4d | |- ( A e. dom card -> ( A e. Fin7 <-> A e. Fin ) ) |