Description: If the Axiom of Infinity is negated, then the class of all natural numbers equals the proper class of all ordinal numbers. (Contributed by BTernaryTau, 30-Dec-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fineqvomon | |- ( Fin = _V -> _om = On ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | onfin2 | |- _om = ( On i^i Fin ) |
|
| 2 | ineq2 | |- ( Fin = _V -> ( On i^i Fin ) = ( On i^i _V ) ) |
|
| 3 | inv1 | |- ( On i^i _V ) = On |
|
| 4 | 2 3 | eqtrdi | |- ( Fin = _V -> ( On i^i Fin ) = On ) |
| 5 | 1 4 | eqtrid | |- ( Fin = _V -> _om = On ) |