Metamath Proof Explorer

Theorem alephexp1

Description: An exponentiation law for alephs. Lemma 6.1 of Jech p. 42. (Contributed by NM, 29-Sep-2004) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion alephexp1 
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( ( aleph ` A ) ^m ( aleph ` B ) ) ~~ ( 2o ^m ( aleph ` B ) ) )

Proof

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