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