Metamath Proof Explorer

Theorem hauspwdom

Description: Simplify the cardinal A ^ NN of hausmapdom to ~P B = 2 ^ B when B is an infinite cardinal greater than A . (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypothesis hauspwdom.1 
|- X = U. J
Assertion hauspwdom 
|- ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> ( ( cls ` J ) ` A ) ~<_ ~P B )

Proof

Step Hyp Ref Expression
1 hauspwdom.1 
 |-  X = U. J
2 1 hausmapdom 
 |-  ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) -> ( ( cls ` J ) ` A ) ~<_ ( A ^m NN ) )
3 2 adantr 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> ( ( cls ` J ) ` A ) ~<_ ( A ^m NN ) )
4 simprr 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> NN ~<_ B )
5 1nn 
 |-  1 e. NN
6 noel 
 |-  -. 1 e. (/)
7 eleq2 
 |-  ( NN = (/) -> ( 1 e. NN <-> 1 e. (/) ) )
8 6 7 mtbiri 
 |-  ( NN = (/) -> -. 1 e. NN )
9 8 adantr 
 |-  ( ( NN = (/) /\ A = (/) ) -> -. 1 e. NN )
10 5 9 mt2 
 |-  -. ( NN = (/) /\ A = (/) )
11 mapdom2 
 |-  ( ( NN ~<_ B /\ -. ( NN = (/) /\ A = (/) ) ) -> ( A ^m NN ) ~<_ ( A ^m B ) )
12 4 10 11 sylancl 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> ( A ^m NN ) ~<_ ( A ^m B ) )
13 sdomdom 
 |-  ( A ~< 2o -> A ~<_ 2o )
14 13 adantl 
 |-  ( ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) /\ A ~< 2o ) -> A ~<_ 2o )
15 mapdom1 
 |-  ( A ~<_ 2o -> ( A ^m B ) ~<_ ( 2o ^m B ) )
16 14 15 syl 
 |-  ( ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) /\ A ~< 2o ) -> ( A ^m B ) ~<_ ( 2o ^m B ) )
17 reldom 
 |-  Rel ~<_
18 17 brrelex2i 
 |-  ( NN ~<_ B -> B e. _V )
19 18 ad2antll 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> B e. _V )
20 pw2eng 
 |-  ( B e. _V -> ~P B ~~ ( 2o ^m B ) )
21 ensym 
 |-  ( ~P B ~~ ( 2o ^m B ) -> ( 2o ^m B ) ~~ ~P B )
22 19 20 21 3syl 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> ( 2o ^m B ) ~~ ~P B )
23 22 adantr 
 |-  ( ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) /\ A ~< 2o ) -> ( 2o ^m B ) ~~ ~P B )
24 domentr 
 |-  ( ( ( A ^m B ) ~<_ ( 2o ^m B ) /\ ( 2o ^m B ) ~~ ~P B ) -> ( A ^m B ) ~<_ ~P B )
25 16 23 24 syl2anc 
 |-  ( ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) /\ A ~< 2o ) -> ( A ^m B ) ~<_ ~P B )
26 onfin2 
 |-  _om = ( On i^i Fin )
27 inss2 
 |-  ( On i^i Fin ) C_ Fin
28 26 27 eqsstri 
 |-  _om C_ Fin
29 2onn 
 |-  2o e. _om
30 28 29 sselii 
 |-  2o e. Fin
31 simprl 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> A ~<_ ~P B )
32 17 brrelex1i 
 |-  ( A ~<_ ~P B -> A e. _V )
33 31 32 syl 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> A e. _V )
34 fidomtri 
 |-  ( ( 2o e. Fin /\ A e. _V ) -> ( 2o ~<_ A <-> -. A ~< 2o ) )
35 30 33 34 sylancr 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> ( 2o ~<_ A <-> -. A ~< 2o ) )
36 35 biimpar 
 |-  ( ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) /\ -. A ~< 2o ) -> 2o ~<_ A )
37 numth3 
 |-  ( B e. _V -> B e. dom card )
38 19 37 syl 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> B e. dom card )
39 38 adantr 
 |-  ( ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) /\ 2o ~<_ A ) -> B e. dom card )
40 nnenom 
 |-  NN ~~ _om
41 40 ensymi 
 |-  _om ~~ NN
42 endomtr 
 |-  ( ( _om ~~ NN /\ NN ~<_ B ) -> _om ~<_ B )
43 41 4 42 sylancr 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> _om ~<_ B )
44 43 adantr 
 |-  ( ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) /\ 2o ~<_ A ) -> _om ~<_ B )
45 simpr 
 |-  ( ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) /\ 2o ~<_ A ) -> 2o ~<_ A )
46 31 adantr 
 |-  ( ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) /\ 2o ~<_ A ) -> A ~<_ ~P B )
47 mappwen 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( 2o ~<_ A /\ A ~<_ ~P B ) ) -> ( A ^m B ) ~~ ~P B )
48 39 44 45 46 47 syl22anc 
 |-  ( ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) /\ 2o ~<_ A ) -> ( A ^m B ) ~~ ~P B )
49 endom 
 |-  ( ( A ^m B ) ~~ ~P B -> ( A ^m B ) ~<_ ~P B )
50 48 49 syl 
 |-  ( ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) /\ 2o ~<_ A ) -> ( A ^m B ) ~<_ ~P B )
51 36 50 syldan 
 |-  ( ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) /\ -. A ~< 2o ) -> ( A ^m B ) ~<_ ~P B )
52 25 51 pm2.61dan 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> ( A ^m B ) ~<_ ~P B )
53 domtr 
 |-  ( ( ( A ^m NN ) ~<_ ( A ^m B ) /\ ( A ^m B ) ~<_ ~P B ) -> ( A ^m NN ) ~<_ ~P B )
54 12 52 53 syl2anc 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> ( A ^m NN ) ~<_ ~P B )
55 domtr 
 |-  ( ( ( ( cls ` J ) ` A ) ~<_ ( A ^m NN ) /\ ( A ^m NN ) ~<_ ~P B ) -> ( ( cls ` J ) ` A ) ~<_ ~P B )
56 3 54 55 syl2anc 
 |-  ( ( ( J e. Haus /\ J e. 1stc /\ A C_ X ) /\ ( A ~<_ ~P B /\ NN ~<_ B ) ) -> ( ( cls ` J ) ` A ) ~<_ ~P B )