Metamath Proof Explorer

Theorem isinfcard

Description: Two ways to express the property of being a transfinite cardinal. (Contributed by NM, 9-Nov-2003)

Ref Expression
Assertion isinfcard 
|- ( ( _om C_ A /\ ( card ` A ) = A ) <-> A e. ran aleph )

Proof

Step Hyp Ref Expression
1 alephfnon 
 |-  aleph Fn On
2 fvelrnb 
 |-  ( aleph Fn On -> ( A e. ran aleph <-> E. x e. On ( aleph ` x ) = A ) )
3 1 2 ax-mp 
 |-  ( A e. ran aleph <-> E. x e. On ( aleph ` x ) = A )
4 alephgeom 
 |-  ( x e. On <-> _om C_ ( aleph ` x ) )
5 4 biimpi 
 |-  ( x e. On -> _om C_ ( aleph ` x ) )
6 sseq2 
 |-  ( A = ( aleph ` x ) -> ( _om C_ A <-> _om C_ ( aleph ` x ) ) )
7 5 6 syl5ibrcom 
 |-  ( x e. On -> ( A = ( aleph ` x ) -> _om C_ A ) )
8 7 rexlimiv 
 |-  ( E. x e. On A = ( aleph ` x ) -> _om C_ A )
9 8 pm4.71ri 
 |-  ( E. x e. On A = ( aleph ` x ) <-> ( _om C_ A /\ E. x e. On A = ( aleph ` x ) ) )
10 eqcom 
 |-  ( ( aleph ` x ) = A <-> A = ( aleph ` x ) )
11 10 rexbii 
 |-  ( E. x e. On ( aleph ` x ) = A <-> E. x e. On A = ( aleph ` x ) )
12 cardalephex 
 |-  ( _om C_ A -> ( ( card ` A ) = A <-> E. x e. On A = ( aleph ` x ) ) )
13 12 pm5.32i 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) <-> ( _om C_ A /\ E. x e. On A = ( aleph ` x ) ) )
14 9 11 13 3bitr4i 
 |-  ( E. x e. On ( aleph ` x ) = A <-> ( _om C_ A /\ ( card ` A ) = A ) )
15 3 14 bitr2i 
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) <-> A e. ran aleph )