Description: The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004) (Revised by Mario Carneiro, 9-Mar-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xpnnen | |- ( NN X. NN ) ~~ NN |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nnenom | |- NN ~~ _om |
|
| 2 | xpen | |- ( ( NN ~~ _om /\ NN ~~ _om ) -> ( NN X. NN ) ~~ ( _om X. _om ) ) |
|
| 3 | 1 1 2 | mp2an | |- ( NN X. NN ) ~~ ( _om X. _om ) |
| 4 | xpomen | |- ( _om X. _om ) ~~ _om |
|
| 5 | 4 1 | entr4i | |- ( _om X. _om ) ~~ NN |
| 6 | 3 5 | entri | |- ( NN X. NN ) ~~ NN |