Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  infenaleph Structured version   Unicode version

Theorem infenaleph 8253
 Description: An infinite numerable set is equinumerous to an infinite initial ordinal. (Contributed by Jeff Hankins, 23-Oct-2009.) (Revised by Mario Carneiro, 29-Apr-2015.)
Assertion
Ref Expression
infenaleph
Distinct variable group:   ,

Proof of Theorem infenaleph
StepHypRef Expression
1 cardidm 8121 . . . . 5
2 cardom 8148 . . . . . . 7
3 simpr 461 . . . . . . . 8
4 omelon 7844 . . . . . . . . . 10
5 onenon 8111 . . . . . . . . . 10
64, 5ax-mp 5 . . . . . . . . 9
7 simpl 457 . . . . . . . . 9
8 carddom2 8139 . . . . . . . . 9
96, 7, 8sylancr 663 . . . . . . . 8
103, 9mpbird 232 . . . . . . 7
112, 10syl5eqssr 3396 . . . . . 6
12 cardalephex 8252 . . . . . 6
1311, 12syl 16 . . . . 5
141, 13mpbii 211 . . . 4
15 eqcom 2440 . . . . 5
1615rexbii 2735 . . . 4
1714, 16sylib 196 . . 3
18 alephfnon 8227 . . . 4
19 fvelrnb 5734 . . . 4
2018, 19ax-mp 5 . . 3
2117, 20sylibr 212 . 2
22 cardid2 8115 . . 3