Step |
Hyp |
Ref |
Expression |
1 |
|
alephon |
|- ( aleph ` B ) e. On |
2 |
|
onenon |
|- ( ( aleph ` B ) e. On -> ( aleph ` B ) e. dom card ) |
3 |
1 2
|
mp1i |
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( aleph ` B ) e. dom card ) |
4 |
|
fvex |
|- ( aleph ` B ) e. _V |
5 |
|
simplr |
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> B e. On ) |
6 |
|
alephgeom |
|- ( B e. On <-> _om C_ ( aleph ` B ) ) |
7 |
5 6
|
sylib |
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> _om C_ ( aleph ` B ) ) |
8 |
|
ssdomg |
|- ( ( aleph ` B ) e. _V -> ( _om C_ ( aleph ` B ) -> _om ~<_ ( aleph ` B ) ) ) |
9 |
4 7 8
|
mpsyl |
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> _om ~<_ ( aleph ` B ) ) |
10 |
|
fvex |
|- ( aleph ` A ) e. _V |
11 |
|
ordom |
|- Ord _om |
12 |
|
2onn |
|- 2o e. _om |
13 |
|
ordelss |
|- ( ( Ord _om /\ 2o e. _om ) -> 2o C_ _om ) |
14 |
11 12 13
|
mp2an |
|- 2o C_ _om |
15 |
|
simpll |
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> A e. On ) |
16 |
|
alephgeom |
|- ( A e. On <-> _om C_ ( aleph ` A ) ) |
17 |
15 16
|
sylib |
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> _om C_ ( aleph ` A ) ) |
18 |
14 17
|
sstrid |
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> 2o C_ ( aleph ` A ) ) |
19 |
|
ssdomg |
|- ( ( aleph ` A ) e. _V -> ( 2o C_ ( aleph ` A ) -> 2o ~<_ ( aleph ` A ) ) ) |
20 |
10 18 19
|
mpsyl |
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> 2o ~<_ ( aleph ` A ) ) |
21 |
|
alephord3 |
|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( aleph ` A ) C_ ( aleph ` B ) ) ) |
22 |
|
ssdomg |
|- ( ( aleph ` B ) e. _V -> ( ( aleph ` A ) C_ ( aleph ` B ) -> ( aleph ` A ) ~<_ ( aleph ` B ) ) ) |
23 |
4 22
|
ax-mp |
|- ( ( aleph ` A ) C_ ( aleph ` B ) -> ( aleph ` A ) ~<_ ( aleph ` B ) ) |
24 |
21 23
|
syl6bi |
|- ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( aleph ` A ) ~<_ ( aleph ` B ) ) ) |
25 |
24
|
imp |
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( aleph ` A ) ~<_ ( aleph ` B ) ) |
26 |
4
|
canth2 |
|- ( aleph ` B ) ~< ~P ( aleph ` B ) |
27 |
|
sdomdom |
|- ( ( aleph ` B ) ~< ~P ( aleph ` B ) -> ( aleph ` B ) ~<_ ~P ( aleph ` B ) ) |
28 |
26 27
|
ax-mp |
|- ( aleph ` B ) ~<_ ~P ( aleph ` B ) |
29 |
|
domtr |
|- ( ( ( aleph ` A ) ~<_ ( aleph ` B ) /\ ( aleph ` B ) ~<_ ~P ( aleph ` B ) ) -> ( aleph ` A ) ~<_ ~P ( aleph ` B ) ) |
30 |
25 28 29
|
sylancl |
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( aleph ` A ) ~<_ ~P ( aleph ` B ) ) |
31 |
|
mappwen |
|- ( ( ( ( aleph ` B ) e. dom card /\ _om ~<_ ( aleph ` B ) ) /\ ( 2o ~<_ ( aleph ` A ) /\ ( aleph ` A ) ~<_ ~P ( aleph ` B ) ) ) -> ( ( aleph ` A ) ^m ( aleph ` B ) ) ~~ ~P ( aleph ` B ) ) |
32 |
3 9 20 30 31
|
syl22anc |
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( ( aleph ` A ) ^m ( aleph ` B ) ) ~~ ~P ( aleph ` B ) ) |
33 |
4
|
pw2en |
|- ~P ( aleph ` B ) ~~ ( 2o ^m ( aleph ` B ) ) |
34 |
|
enen2 |
|- ( ~P ( aleph ` B ) ~~ ( 2o ^m ( aleph ` B ) ) -> ( ( ( aleph ` A ) ^m ( aleph ` B ) ) ~~ ~P ( aleph ` B ) <-> ( ( aleph ` A ) ^m ( aleph ` B ) ) ~~ ( 2o ^m ( aleph ` B ) ) ) ) |
35 |
33 34
|
ax-mp |
|- ( ( ( aleph ` A ) ^m ( aleph ` B ) ) ~~ ~P ( aleph ` B ) <-> ( ( aleph ` A ) ^m ( aleph ` B ) ) ~~ ( 2o ^m ( aleph ` B ) ) ) |
36 |
32 35
|
sylib |
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( ( aleph ` A ) ^m ( aleph ` B ) ) ~~ ( 2o ^m ( aleph ` B ) ) ) |