Metamath Proof Explorer


Theorem cardalephex

Description: Every transfinite cardinal is an aleph and vice-versa. Theorem 8A(b) of Enderton p. 213 and its converse. (Contributed by NM, 5-Nov-2003)

Ref Expression
Assertion cardalephex
|- ( _om C_ A -> ( ( card ` A ) = A <-> E. x e. On A = ( aleph ` x ) ) )

Proof

Step Hyp Ref Expression
1 simpl
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> _om C_ A )
2 cardaleph
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> A = ( aleph ` |^| { y e. On | A C_ ( aleph ` y ) } ) )
3 2 sseq2d
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> ( _om C_ A <-> _om C_ ( aleph ` |^| { y e. On | A C_ ( aleph ` y ) } ) ) )
4 alephgeom
 |-  ( |^| { y e. On | A C_ ( aleph ` y ) } e. On <-> _om C_ ( aleph ` |^| { y e. On | A C_ ( aleph ` y ) } ) )
5 3 4 bitr4di
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> ( _om C_ A <-> |^| { y e. On | A C_ ( aleph ` y ) } e. On ) )
6 1 5 mpbid
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> |^| { y e. On | A C_ ( aleph ` y ) } e. On )
7 fveq2
 |-  ( x = |^| { y e. On | A C_ ( aleph ` y ) } -> ( aleph ` x ) = ( aleph ` |^| { y e. On | A C_ ( aleph ` y ) } ) )
8 7 rspceeqv
 |-  ( ( |^| { y e. On | A C_ ( aleph ` y ) } e. On /\ A = ( aleph ` |^| { y e. On | A C_ ( aleph ` y ) } ) ) -> E. x e. On A = ( aleph ` x ) )
9 6 2 8 syl2anc
 |-  ( ( _om C_ A /\ ( card ` A ) = A ) -> E. x e. On A = ( aleph ` x ) )
10 9 ex
 |-  ( _om C_ A -> ( ( card ` A ) = A -> E. x e. On A = ( aleph ` x ) ) )
11 alephcard
 |-  ( card ` ( aleph ` x ) ) = ( aleph ` x )
12 fveq2
 |-  ( A = ( aleph ` x ) -> ( card ` A ) = ( card ` ( aleph ` x ) ) )
13 id
 |-  ( A = ( aleph ` x ) -> A = ( aleph ` x ) )
14 11 12 13 3eqtr4a
 |-  ( A = ( aleph ` x ) -> ( card ` A ) = A )
15 14 rexlimivw
 |-  ( E. x e. On A = ( aleph ` x ) -> ( card ` A ) = A )
16 10 15 impbid1
 |-  ( _om C_ A -> ( ( card ` A ) = A <-> E. x e. On A = ( aleph ` x ) ) )