This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 ) ) ) |
| 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 ) ) ) |