Metamath Proof Explorer

Theorem infenaleph

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)

Ref Expression
Assertion infenaleph 
|- ( ( A e. dom card /\ _om ~<_ A ) -> E. x e. ran aleph x ~~ A )

Proof

Step Hyp Ref Expression
1 cardidm 
 |-  ( card ` ( card ` A ) ) = ( card ` A )
2 cardom 
 |-  ( card ` _om ) = _om
3 simpr 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> _om ~<_ A )
4 omelon 
 |-  _om e. On
5 onenon 
 |-  ( _om e. On -> _om e. dom card )
6 4 5 ax-mp 
 |-  _om e. dom card
7 simpl 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> A e. dom card )
8 carddom2 
 |-  ( ( _om e. dom card /\ A e. dom card ) -> ( ( card ` _om ) C_ ( card ` A ) <-> _om ~<_ A ) )
9 6 7 8 sylancr 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ( card ` _om ) C_ ( card ` A ) <-> _om ~<_ A ) )
10 3 9 mpbird 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( card ` _om ) C_ ( card ` A ) )
11 2 10 eqsstrrid 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> _om C_ ( card ` A ) )
12 cardalephex 
 |-  ( _om C_ ( card ` A ) -> ( ( card ` ( card ` A ) ) = ( card ` A ) <-> E. x e. On ( card ` A ) = ( aleph ` x ) ) )
13 11 12 syl 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ( card ` ( card ` A ) ) = ( card ` A ) <-> E. x e. On ( card ` A ) = ( aleph ` x ) ) )
14 1 13 mpbii 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> E. x e. On ( card ` A ) = ( aleph ` x ) )
15 eqcom 
 |-  ( ( card ` A ) = ( aleph ` x ) <-> ( aleph ` x ) = ( card ` A ) )
16 15 rexbii 
 |-  ( E. x e. On ( card ` A ) = ( aleph ` x ) <-> E. x e. On ( aleph ` x ) = ( card ` A ) )
17 14 16 sylib 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> E. x e. On ( aleph ` x ) = ( card ` A ) )
18 alephfnon 
 |-  aleph Fn On
19 fvelrnb 
 |-  ( aleph Fn On -> ( ( card ` A ) e. ran aleph <-> E. x e. On ( aleph ` x ) = ( card ` A ) ) )
20 18 19 ax-mp 
 |-  ( ( card ` A ) e. ran aleph <-> E. x e. On ( aleph ` x ) = ( card ` A ) )
21 17 20 sylibr 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( card ` A ) e. ran aleph )
22 cardid2 
 |-  ( A e. dom card -> ( card ` A ) ~~ A )
23 22 adantr 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( card ` A ) ~~ A )
24 breq1 
 |-  ( x = ( card ` A ) -> ( x ~~ A <-> ( card ` A ) ~~ A ) )
25 24 rspcev 
 |-  ( ( ( card ` A ) e. ran aleph /\ ( card ` A ) ~~ A ) -> E. x e. ran aleph x ~~ A )
26 21 23 25 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> E. x e. ran aleph x ~~ A )