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