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

Theorem mapunen 7747
 Description: Equinumerosity law for set exponentiation of a disjoint union. Exercise 4.45 of [Mendelson] p. 255. (Contributed by NM, 23-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
Assertion
Ref Expression
mapunen

Proof of Theorem mapunen
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovex 6333 . . 3
21a1i 11 . 2
3 ovex 6333 . . . 4
4 ovex 6333 . . . 4
53, 4xpex 6609 . . 3
65a1i 11 . 2
7 elmapi 7501 . . . . 5
8 ssun1 3635 . . . . 5
9 fssres 5766 . . . . 5
107, 8, 9sylancl 666 . . . 4
11 ssun2 3636 . . . . 5
12 fssres 5766 . . . . 5
137, 11, 12sylancl 666 . . . 4
1410, 13jca 534 . . 3
15 opelxp 4884 . . . 4
16 simpl3 1010 . . . . . 6
17 simpl1 1008 . . . . . 6
1816, 17elmapd 7494 . . . . 5
19 simpl2 1009 . . . . . 6
2016, 19elmapd 7494 . . . . 5
2118, 20anbi12d 715 . . . 4
2215, 21syl5bb 260 . . 3
2314, 22syl5ibr 224 . 2
24 xp1st 6837 . . . . . . 7
2524adantl 467 . . . . . 6
26 elmapi 7501 . . . . . 6
2725, 26syl 17 . . . . 5
28 xp2nd 6838 . . . . . . 7
2928adantl 467 . . . . . 6
30 elmapi 7501 . . . . . 6
3129, 30syl 17 . . . . 5
32 simplr 760 . . . . 5
33 fun2 5764 . . . . 5
3427, 31, 32, 33syl21anc 1263 . . . 4
3534ex 435 . . 3
36 unexg 6606 . . . . 5
3717, 19, 36syl2anc 665 . . . 4
3816, 37elmapd 7494 . . 3
3935, 38sylibrd 237 . 2
40 1st2nd2 6844 . . . . . . 7
4140ad2antll 733 . . . . . 6
4227adantrl 720 . . . . . . . 8
4331adantrl 720 . . . . . . . 8
44 res0 5129 . . . . . . . . . 10
45 res0 5129 . . . . . . . . . 10
4644, 45eqtr4i 2461 . . . . . . . . 9
47 simplr 760 . . . . . . . . . 10
4847reseq2d 5125 . . . . . . . . 9
4947reseq2d 5125 . . . . . . . . 9
5046, 48, 493eqtr4a 2496 . . . . . . . 8
51 fresaunres1 5773 . . . . . . . 8
5242, 43, 50, 51syl3anc 1264 . . . . . . 7
53 fresaunres2 5772 . . . . . . . 8
5442, 43, 50, 53syl3anc 1264 . . . . . . 7
5552, 54opeq12d 4198 . . . . . 6
5641, 55eqtr4d 2473 . . . . 5
57 reseq1 5119 . . . . . . 7
58 reseq1 5119 . . . . . . 7
5957, 58opeq12d 4198 . . . . . 6
6059eqeq2d 2443 . . . . 5
6156, 60syl5ibrcom 225 . . . 4
62 ffn 5746 . . . . . . . 8
63 fnresdm 5703 . . . . . . . 8
647, 62, 633syl 18 . . . . . . 7
6564ad2antrl 732 . . . . . 6
6665eqcomd 2437 . . . . 5
67 vex 3090 . . . . . . . . . 10
6867resex 5168 . . . . . . . . 9
6967resex 5168 . . . . . . . . 9
7068, 69op1std 6817 . . . . . . . 8
7168, 69op2ndd 6818 . . . . . . . 8
7270, 71uneq12d 3627 . . . . . . 7
73 resundi 5138 . . . . . . 7
7472, 73syl6eqr 2488 . . . . . 6
7574eqeq2d 2443 . . . . 5
7666, 75syl5ibrcom 225 . . . 4
7761, 76impbid 193 . . 3
7877ex 435 . 2
792, 6, 23, 39, 78en3d 7613 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1870  cvv 3087   cun 3440   cin 3441   wss 3442  c0 3767  cop 4008   class class class wbr 4426   cxp 4852   cres 4856   wfn 5596  wf 5597  cfv 5601  (class class class)co 6305  c1st 6805  c2nd 6806   cmap 7480   cen 7574 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-1st 6807  df-2nd 6808  df-map 7482  df-en 7578 This theorem is referenced by:  map2xp  7748  mapdom2  7749  mapcdaen  8612  ackbij1lem5  8652  hashmap  12602
 Copyright terms: Public domain W3C validator