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

Theorem mapunen 6915
 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
StepHypRef Expression
1 ovex 5735 . . 3
21a1i 12 . 2
3 ovex 5735 . . . 4
4 ovex 5735 . . . 4
53, 4xpex 4708 . . 3
65a1i 12 . 2
7 elmapi 6678 . . . . 5
8 ssun1 3248 . . . . 5
9 fssres 5265 . . . . 5
107, 8, 9sylancl 646 . . . 4
11 ssun2 3249 . . . . 5
12 fssres 5265 . . . . 5
137, 11, 12sylancl 646 . . . 4
1410, 13jca 520 . . 3
15 opelxp 4626 . . . 4
16 simpl3 965 . . . . . 6
17 simpl1 963 . . . . . 6
18 elmapg 6671 . . . . . 6
1916, 17, 18syl2anc 645 . . . . 5
20 simpl2 964 . . . . . 6
21 elmapg 6671 . . . . . 6
2216, 20, 21syl2anc 645 . . . . 5
2319, 22anbi12d 694 . . . 4
2415, 23syl5bb 250 . . 3
2514, 24syl5ibr 214 . 2
26 xp1st 6001 . . . . . . 7
2726adantl 454 . . . . . 6
28 elmapi 6678 . . . . . 6
2927, 28syl 17 . . . . 5
30 xp2nd 6002 . . . . . . 7
3130adantl 454 . . . . . 6
32 elmapi 6678 . . . . . 6
3331, 32syl 17 . . . . 5
34 simplr 734 . . . . 5
35 fun2 5263 . . . . 5
3629, 33, 34, 35syl21anc 1186 . . . 4
3736ex 425 . . 3
38 unexg 4412 . . . . 5
3917, 20, 38syl2anc 645 . . . 4
40 elmapg 6671 . . . 4
4116, 39, 40syl2anc 645 . . 3
4237, 41sylibrd 227 . 2
43 1st2nd2 6011 . . . . . . 7
4443ad2antll 712 . . . . . 6
4529adantrl 699 . . . . . . . 8
4633adantrl 699 . . . . . . . 8
47 res0 4866 . . . . . . . . . 10
48 res0 4866 . . . . . . . . . 10
4947, 48eqtr4i 2276 . . . . . . . . 9
50 simplr 734 . . . . . . . . . 10
5150reseq2d 4862 . . . . . . . . 9
5250reseq2d 4862 . . . . . . . . 9
5349, 51, 523eqtr4a 2311 . . . . . . . 8
54 fresaunres1 5271 . . . . . . . 8
5545, 46, 53, 54syl3anc 1187 . . . . . . 7
56 fresaunres2 5270 . . . . . . . 8
5745, 46, 53, 56syl3anc 1187 . . . . . . 7
5855, 57opeq12d 3704 . . . . . 6
5944, 58eqtr4d 2288 . . . . 5
60 reseq1 4856 . . . . . . 7
61 reseq1 4856 . . . . . . 7
6260, 61opeq12d 3704 . . . . . 6
6362eqeq2d 2264 . . . . 5
6459, 63syl5ibrcom 215 . . . 4
65 ffn 5246 . . . . . . . 8
66 fnresdm 5210 . . . . . . . 8
677, 65, 663syl 20 . . . . . . 7
6867ad2antrl 711 . . . . . 6
6968eqcomd 2258 . . . . 5
70 vex 2730 . . . . . . . . . 10
7170resex 4902 . . . . . . . . 9
7270resex 4902 . . . . . . . . 9
7371, 72op1std 5982 . . . . . . . 8
7471, 72op2ndd 5983 . . . . . . . 8
7573, 74uneq12d 3240 . . . . . . 7
76 resundi 4876 . . . . . . 7
7775, 76syl6eqr 2303 . . . . . 6
7877eqeq2d 2264 . . . . 5
7969, 78syl5ibrcom 215 . . . 4
8064, 79impbid 185 . . 3
8180ex 425 . 2
822, 6, 25, 42, 81en3d 6784 1
 Colors of variables: wff set class Syntax hints:   wi 6   wb 178   wa 360   w3a 939   wceq 1619   wcel 1621  cvv 2727   cun 3076   cin 3077   wss 3078  c0 3362  cop 3547   class class class wbr 3920   cxp 4578   cres 4582   wfn 4587  wf 4588  cfv 4592  (class class class)co 5710  c1st 5972  c2nd 5973   cmap 6658   cen 6746 This theorem is referenced by:  map2xp  6916  mapdom2  6917  mapcdaen  7694  ackbij1lem5  7734  hashmap  11264 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pow 4082  ax-pr 4108  ax-un 4403 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-csb 3010  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-iun 3805  df-br 3921  df-opab 3975  df-mpt 3976  df-id 4202  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fn 4603  df-f 4604  df-f1 4605  df-fo 4606  df-f1o 4607  df-fv 4608  df-ov 5713  df-oprab 5714  df-mpt2 5715  df-1st 5974  df-2nd 5975  df-map 6660  df-en 6750
 Copyright terms: Public domain W3C validator