Description: Value of the cofinality function at omega (the set of natural numbers). Exercise 4 of TakeutiZaring p. 102. (Contributed by NM, 23-Apr-2004) (Proof shortened by Mario Carneiro, 11-Jun-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cfom | |- ( cf ` _om ) = _om |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cfle | |- ( cf ` _om ) C_ _om |
|
| 2 | limom | |- Lim _om |
|
| 3 | omex | |- _om e. _V |
|
| 4 | 3 | cflim2 | |- ( Lim _om <-> Lim ( cf ` _om ) ) |
| 5 | 2 4 | mpbi | |- Lim ( cf ` _om ) |
| 6 | limomss | |- ( Lim ( cf ` _om ) -> _om C_ ( cf ` _om ) ) |
|
| 7 | 5 6 | ax-mp | |- _om C_ ( cf ` _om ) |
| 8 | 1 7 | eqssi | |- ( cf ` _om ) = _om |