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

Theorem mapxpen 7703
Description: Equinumerosity law for double set exponentiation. Proposition 10.45 of [TakeutiZaring] p. 96. (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2015.)
Assertion
Ref Expression
mapxpen

Proof of Theorem mapxpen
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovex 6324 . . 3
21a1i 11 . 2
3 ovex 6324 . . 3
43a1i 11 . 2
5 elmapi 7460 . . . . . . . . . 10
65ffvelrnda 6031 . . . . . . . . 9
7 elmapi 7460 . . . . . . . . 9
86, 7syl 16 . . . . . . . 8
98ffvelrnda 6031 . . . . . . 7
109an32s 804 . . . . . 6
1110ralrimiva 2871 . . . . 5
1211ralrimiva 2871 . . . 4
13 eqid 2457 . . . . 5
1413fmpt2 6867 . . . 4
1512, 14sylib 196 . . 3
16 simp1 996 . . . 4
17 xpexg 6602 . . . . 5
18173adant1 1014 . . . 4
19 elmapg 7452 . . . 4
2016, 18, 19syl2anc 661 . . 3
2115, 20syl5ibr 221 . 2
22 elmapi 7460 . . . . . . . . 9
2322adantl 466 . . . . . . . 8
24 fovrn 6445 . . . . . . . . . 10
25243expa 1196 . . . . . . . . 9
2625an32s 804 . . . . . . . 8
2723, 26sylanl1 650 . . . . . . 7
28 eqid 2457 . . . . . . 7
2927, 28fmptd 6055 . . . . . 6
30 elmapg 7452 . . . . . . . 8
31303adant3 1016 . . . . . . 7
3231ad2antrr 725 . . . . . 6
3329, 32mpbird 232 . . . . 5
34 eqid 2457 . . . . 5
3533, 34fmptd 6055 . . . 4
3635ex 434 . . 3
37 ovex 6324 . . . 4
38 simp3 998 . . . 4
39 elmapg 7452 . . . 4
4037, 38, 39sylancr 663 . . 3
4136, 40sylibrd 234 . 2
42 elmapfn 7461 . . . . . . . 8
4342ad2antll 728 . . . . . . 7
44 fnov 6410 . . . . . . 7
4543, 44sylib 196 . . . . . 6
46 simp3 998 . . . . . . . . . 10
4729adantlrl 719 . . . . . . . . . . . 12
48473adant2 1015 . . . . . . . . . . 11
49 simp1l2 1090 . . . . . . . . . . 11
50 simp1l1 1089 . . . . . . . . . . 11
51 fex2 6755 . . . . . . . . . . 11
5248, 49, 50, 51syl3anc 1228 . . . . . . . . . 10
5334fvmpt2 5963 . . . . . . . . . 10
5446, 52, 53syl2anc 661 . . . . . . . . 9
5554fveq1d 5873 . . . . . . . 8
56 simp2 997 . . . . . . . . 9
57 ovex 6324 . . . . . . . . 9
5828fvmpt2 5963 . . . . . . . . 9
5956, 57, 58sylancl 662 . . . . . . . 8
6055, 59eqtrd 2498 . . . . . . 7
6160mpt2eq3dva 6361 . . . . . 6
6245, 61eqtr4d 2501 . . . . 5
63 eqid 2457 . . . . . . 7
64 nfcv 2619 . . . . . . . . . 10
65 nfmpt1 4541 . . . . . . . . . 10
6664, 65nfmpt 4540 . . . . . . . . 9
6766nfeq2 2636 . . . . . . . 8
68 nfmpt1 4541 . . . . . . . . . . . 12
6968nfeq2 2636 . . . . . . . . . . 11
70 fveq1 5870 . . . . . . . . . . . . 13
7170fveq1d 5873 . . . . . . . . . . . 12
7271a1d 25 . . . . . . . . . . 11
7369, 72ralrimi 2857 . . . . . . . . . 10
74 eqid 2457 . . . . . . . . . 10
7573, 74jctil 537 . . . . . . . . 9
7675a1d 25 . . . . . . . 8
7767, 76ralrimi 2857 . . . . . . 7
78 mpt2eq123 6356 . . . . . . 7
7963, 77, 78sylancr 663 . . . . . 6
8079eqeq2d 2471 . . . . 5
8162, 80syl5ibrcom 222 . . . 4
825ad2antrl 727 . . . . . . 7
8382feqmptd 5926 . . . . . 6
84 simprl 756 . . . . . . . . 9
8584, 8sylan 471 . . . . . . . 8
8685feqmptd 5926 . . . . . . 7
8786mpteq2dva 4538 . . . . . 6
8883, 87eqtrd 2498 . . . . 5
89 nfmpt22 6365 . . . . . . . . 9
9089nfeq2 2636 . . . . . . . 8
91 eqidd 2458 . . . . . . . . 9
92 nfmpt21 6364 . . . . . . . . . . 11
9392nfeq2 2636 . . . . . . . . . 10
94 nfv 1707 . . . . . . . . . 10
95 fvex 5881 . . . . . . . . . . . . 13
9613ovmpt4g 6425 . . . . . . . . . . . . 13
9795, 96mp3an3 1313 . . . . . . . . . . . 12
98 oveq 6302 . . . . . . . . . . . . 13
9998eqeq1d 2459 . . . . . . . . . . . 12
10097, 99syl5ibr 221 . . . . . . . . . . 11
101100expcomd 438 . . . . . . . . . 10
10293, 94, 101ralrimd 2861 . . . . . . . . 9
103 mpteq12 4531 . . . . . . . . 9
10491, 102, 103syl6an 545 . . . . . . . 8
10590, 104ralrimi 2857 . . . . . . 7
106 mpteq12 4531 . . . . . . 7
10774, 105, 106sylancr 663 . . . . . 6
108107eqeq2d 2471 . . . . 5
10988, 108syl5ibrcom 222 . . . 4
11081, 109impbid 191 . . 3
111110ex 434 . 2
1122, 4, 21, 41, 111en3d 7572 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  A.wral 2807   cvv 3109   class class class wbr 4452  e.cmpt 4510  X.cxp 5002  Fnwfn 5588  -->wf 5589  `cfv 5593  (class class class)co 6296  e.cmpt2 6298   cmap 7439   cen 7533
This theorem is referenced by:  mappwen  8514  cfpwsdom  8980  rpnnen  13960  rexpen  13961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-1st 6800  df-2nd 6801  df-map 7441  df-en 7537
  Copyright terms: Public domain W3C validator