Step |
Hyp |
Ref |
Expression |
1 |
|
sdomirr |
|- -. _om ~< _om |
2 |
|
2onn |
|- 2o e. _om |
3 |
2
|
elexi |
|- 2o e. _V |
4 |
|
domrefg |
|- ( 2o e. _V -> 2o ~<_ 2o ) |
5 |
3
|
cfpwsdom |
|- ( 2o ~<_ 2o -> ( aleph ` (/) ) ~< ( cf ` ( card ` ( 2o ^m ( aleph ` (/) ) ) ) ) ) |
6 |
3 4 5
|
mp2b |
|- ( aleph ` (/) ) ~< ( cf ` ( card ` ( 2o ^m ( aleph ` (/) ) ) ) ) |
7 |
|
aleph0 |
|- ( aleph ` (/) ) = _om |
8 |
7
|
a1i |
|- ( ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) -> ( aleph ` (/) ) = _om ) |
9 |
7
|
oveq2i |
|- ( 2o ^m ( aleph ` (/) ) ) = ( 2o ^m _om ) |
10 |
9
|
fveq2i |
|- ( card ` ( 2o ^m ( aleph ` (/) ) ) ) = ( card ` ( 2o ^m _om ) ) |
11 |
10
|
eqeq1i |
|- ( ( card ` ( 2o ^m ( aleph ` (/) ) ) ) = ( aleph ` _om ) <-> ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) ) |
12 |
11
|
biimpri |
|- ( ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) -> ( card ` ( 2o ^m ( aleph ` (/) ) ) ) = ( aleph ` _om ) ) |
13 |
12
|
fveq2d |
|- ( ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) -> ( cf ` ( card ` ( 2o ^m ( aleph ` (/) ) ) ) ) = ( cf ` ( aleph ` _om ) ) ) |
14 |
|
limom |
|- Lim _om |
15 |
|
alephsing |
|- ( Lim _om -> ( cf ` ( aleph ` _om ) ) = ( cf ` _om ) ) |
16 |
14 15
|
ax-mp |
|- ( cf ` ( aleph ` _om ) ) = ( cf ` _om ) |
17 |
|
cfom |
|- ( cf ` _om ) = _om |
18 |
16 17
|
eqtri |
|- ( cf ` ( aleph ` _om ) ) = _om |
19 |
13 18
|
eqtrdi |
|- ( ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) -> ( cf ` ( card ` ( 2o ^m ( aleph ` (/) ) ) ) ) = _om ) |
20 |
8 19
|
breq12d |
|- ( ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) -> ( ( aleph ` (/) ) ~< ( cf ` ( card ` ( 2o ^m ( aleph ` (/) ) ) ) ) <-> _om ~< _om ) ) |
21 |
6 20
|
mpbii |
|- ( ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) -> _om ~< _om ) |
22 |
21
|
necon3bi |
|- ( -. _om ~< _om -> ( card ` ( 2o ^m _om ) ) =/= ( aleph ` _om ) ) |
23 |
1 22
|
ax-mp |
|- ( card ` ( 2o ^m _om ) ) =/= ( aleph ` _om ) |