Description: The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of Enderton p. 133. (Contributed by NM, 23-Jul-2004) (Revised by Mario Carneiro, 9-Mar-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xpomen | |- ( _om X. _om ) ~~ _om |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | omelon | |- _om e. On |
|
| 2 | ssid | |- _om C_ _om |
|
| 3 | infxpen | |- ( ( _om e. On /\ _om C_ _om ) -> ( _om X. _om ) ~~ _om ) |
|
| 4 | 1 2 3 | mp2an | |- ( _om X. _om ) ~~ _om |