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 ) ) )