Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  infmap2 Structured version   Unicode version

Theorem infmap2 8594
 Description: An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. Although this version of infmap 8947 avoids the axiom of choice, it requires the powerset of an infinite set to be well-orderable and so is usually not applicable. (Contributed by NM, 1-Oct-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
Assertion
Ref Expression
infmap2
Distinct variable groups:   ,   ,

Proof of Theorem infmap2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 oveq2 6290 . . 3
2 breq2 4451 . . . . 5
32anbi2d 703 . . . 4
43abbidv 2603 . . 3
51, 4breq12d 4460 . 2
6 simpl2 1000 . . . . . . . . . 10
7 reldom 7519 . . . . . . . . . . 11
87brrelexi 5039 . . . . . . . . . 10
96, 8syl 16 . . . . . . . . 9
107brrelex2i 5040 . . . . . . . . . 10
116, 10syl 16 . . . . . . . . 9
12 xpcomeng 7606 . . . . . . . . 9
139, 11, 12syl2anc 661 . . . . . . . 8
14 simpl3 1001 . . . . . . . . . 10
15 simpr 461 . . . . . . . . . . 11
16 mapdom3 7686 . . . . . . . . . . 11
1711, 9, 15, 16syl3anc 1228 . . . . . . . . . 10
18 numdom 8415 . . . . . . . . . 10
1914, 17, 18syl2anc 661 . . . . . . . . 9
20 simpl1 999 . . . . . . . . 9
21 infxpabs 8588 . . . . . . . . 9
2219, 20, 15, 6, 21syl22anc 1229 . . . . . . . 8
23 entr 7564 . . . . . . . 8
2413, 22, 23syl2anc 661 . . . . . . 7
25 ssenen 7688 . . . . . . 7
2624, 25syl 16 . . . . . 6
27 relen 7518 . . . . . . 7
2827brrelexi 5039 . . . . . 6
2926, 28syl 16 . . . . 5
30 abid2 2607 . . . . . 6
31 elmapi 7437 . . . . . . . 8
32 fssxp 5741 . . . . . . . . 9
33 ffun 5731 . . . . . . . . . . 11
34 vex 3116 . . . . . . . . . . . 12
3534fundmen 7586 . . . . . . . . . . 11
36 ensym 7561 . . . . . . . . . . 11
3733, 35, 363syl 20 . . . . . . . . . 10
38 fdm 5733 . . . . . . . . . 10
3937, 38breqtrd 4471 . . . . . . . . 9
4032, 39jca 532 . . . . . . . 8
4131, 40syl 16 . . . . . . 7
4241ss2abi 3572 . . . . . 6
4330, 42eqsstr3i 3535 . . . . 5
44 ssdomg 7558 . . . . 5
4529, 43, 44mpisyl 18 . . . 4
46 domentr 7571 . . . 4
4745, 26, 46syl2anc 661 . . 3
48 ovex 6307 . . . . . . 7
4948mptex 6129 . . . . . 6
5049rnex 6715 . . . . 5
51 ensym 7561 . . . . . . . . . . . 12
5251ad2antll 728 . . . . . . . . . . 11
53 bren 7522 . . . . . . . . . . 11
5452, 53sylib 196 . . . . . . . . . 10
55 f1of 5814 . . . . . . . . . . . . . . . 16
5655adantl 466 . . . . . . . . . . . . . . 15
57 simplrl 759 . . . . . . . . . . . . . . 15
58 fss 5737 . . . . . . . . . . . . . . 15
5956, 57, 58syl2anc 661 . . . . . . . . . . . . . 14
60 elmapg 7430 . . . . . . . . . . . . . . . 16
6111, 9, 60syl2anc 661 . . . . . . . . . . . . . . 15
6261ad2antrr 725 . . . . . . . . . . . . . 14
6359, 62mpbird 232 . . . . . . . . . . . . 13
64 f1ofo 5821 . . . . . . . . . . . . . . . 16
65 forn 5796 . . . . . . . . . . . . . . . 16
6664, 65syl 16 . . . . . . . . . . . . . . 15
6766adantl 466 . . . . . . . . . . . . . 14
6867eqcomd 2475 . . . . . . . . . . . . 13
6963, 68jca 532 . . . . . . . . . . . 12
7069ex 434 . . . . . . . . . . 11
7170eximdv 1686 . . . . . . . . . 10
7254, 71mpd 15 . . . . . . . . 9
73 df-rex 2820 . . . . . . . . 9
7472, 73sylibr 212 . . . . . . . 8
7574ex 434 . . . . . . 7
7675ss2abdv 3573 . . . . . 6
77 eqid 2467 . . . . . . 7
7877rnmpt 5246 . . . . . 6
7976, 78syl6sseqr 3551 . . . . 5
80 ssdomg 7558 . . . . 5
8150, 79, 80mpsyl 63 . . . 4
82 vex 3116 . . . . . . . . 9
8382rnex 6715 . . . . . . . 8
8483rgenw 2825 . . . . . . 7
8577fnmpt 5705 . . . . . . 7
8684, 85mp1i 12 . . . . . 6
87 dffn4 5799 . . . . . 6
8886, 87sylib 196 . . . . 5
89 fodomnum 8434 . . . . 5
9014, 88, 89sylc 60 . . . 4
91 domtr 7565 . . . 4
9281, 90, 91syl2anc 661 . . 3
93 sbth 7634 . . 3
9447, 92, 93syl2anc 661 . 2
957brrelex2i 5040 . . . . 5
96953ad2ant1 1017 . . . 4
97 map0e 7453 . . . 4
9896, 97syl 16 . . 3
99 1onn 7285 . . . . . 6
10099elexi 3123 . . . . 5
101100enref 7545 . . . 4
102 df-sn 4028 . . . . 5
103 df1o2 7139 . . . . 5
104 en0 7575 . . . . . . . 8
105104anbi2i 694 . . . . . . 7
106 0ss 3814 . . . . . . . . 9
107 sseq1 3525 . . . . . . . . 9
108106, 107mpbiri 233 . . . . . . . 8
109108pm4.71ri 633 . . . . . . 7
110105, 109bitr4i 252 . . . . . 6
111110abbii 2601 . . . . 5
112102, 103, 1113eqtr4ri 2507 . . . 4
113101, 112breqtrri 4472 . . 3
11498, 113syl6eqbr 4484 . 2
1155, 94, 114pm2.61ne 2782 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 973   wceq 1379  wex 1596   wcel 1767  cab 2452   wne 2662  wral 2814  wrex 2815  cvv 3113   wss 3476  c0 3785  csn 4027   class class class wbr 4447   cmpt 4505   cxp 4997   cdm 4999   crn 5000   wfun 5580   wfn 5581  wf 5582  wfo 5584  wf1o 5585  (class class class)co 6282  com 6678  c1o 7120   cmap 7417   cen 7510   cdom 7511  ccrd 8312 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-inf2 8054 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-isom 5595  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-er 7308  df-map 7419  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-oi 7931  df-card 8316  df-acn 8319 This theorem is referenced by:  infmap  8947
 Copyright terms: Public domain W3C validator