Description: Under countable choice, the IV-finite sets (Dedekind-finite) coincide with I-finite (finite in the usual sense) sets. (Contributed by Mario Carneiro, 16-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fin41 | |- Fin4 = Fin |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | |- x e. _V |
|
| 2 | 1 | domtriom | |- ( _om ~<_ x <-> -. x ~< _om ) |
| 3 | 2 | con2bii | |- ( x ~< _om <-> -. _om ~<_ x ) |
| 4 | isfinite | |- ( x e. Fin <-> x ~< _om ) |
|
| 5 | isfin4-2 | |- ( x e. _V -> ( x e. Fin4 <-> -. _om ~<_ x ) ) |
|
| 6 | 5 | elv | |- ( x e. Fin4 <-> -. _om ~<_ x ) |
| 7 | 3 4 6 | 3bitr4ri | |- ( x e. Fin4 <-> x e. Fin ) |
| 8 | 7 | eqriv | |- Fin4 = Fin |