Theorem mapunen 7564

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.

Step	Hyp	Ref	Expression
1		ovex 6199	. . 3
2	1	a1i 11	. 2
3		ovex 6199	. . . 4
4		ovex 6199	. . . 4
5	3, 4	xpex 6592	. . 3
6	5	a1i 11	. 2
7		elmapi 7318	. . . . 5
8		ssun1 3601	. . . . 5
9		fssres 5660	. . . . 5
10	7, 8, 9	sylancl 662	. . . 4
11		ssun2 3602	. . . . 5
12		fssres 5660	. . . . 5
13	7, 11, 12	sylancl 662	. . . 4
14	10, 13	jca 532	. . 3
15		opelxp 4951	. . . 4
16		simpl3 993	. . . . . 6
17		simpl1 991	. . . . . 6
18		elmapg 7311	. . . . . 6
19	16, 17, 18	syl2anc 661	. . . . 5
20		simpl2 992	. . . . . 6
21		elmapg 7311	. . . . . 6
22	16, 20, 21	syl2anc 661	. . . . 5
23	19, 22	anbi12d 710	. . . 4
24	15, 23	syl5bb 257	. . 3
25	14, 24	syl5ibr 221	. 2
26		xp1st 6690	. . . . . . 7
27	26	adantl 466	. . . . . 6
28		elmapi 7318	. . . . . 6
29	27, 28	syl 16	. . . . 5
30		xp2nd 6691	. . . . . . 7
31	30	adantl 466	. . . . . 6
32		elmapi 7318	. . . . . 6
33	31, 32	syl 16	. . . . 5
34		simplr 754	. . . . 5
35		fun2 5658	. . . . 5
36	29, 33, 34, 35	syl21anc 1218	. . . 4
37	36	ex 434	. . 3
38		unexg 6465	. . . . 5
39	17, 20, 38	syl2anc 661	. . . 4
40		elmapg 7311	. . . 4
41	16, 39, 40	syl2anc 661	. . 3
42	37, 41	sylibrd 234	. 2
43		1st2nd2 6697	. . . . . . 7
44	43	ad2antll 728	. . . . . 6
45	29	adantrl 715	. . . . . . . 8
46	33	adantrl 715	. . . . . . . 8
47		res0 5197	. . . . . . . . . 10
48		res0 5197	. . . . . . . . . 10
49	47, 48	eqtr4i 2481	. . . . . . . . 9
50		simplr 754	. . . . . . . . . 10
51	50	reseq2d 5192	. . . . . . . . 9
52	50	reseq2d 5192	. . . . . . . . 9
53	49, 51, 52	3eqtr4a 2516	. . . . . . . 8
54		fresaunres1 5666	. . . . . . . 8
55	45, 46, 53, 54	syl3anc 1219	. . . . . . 7
56		fresaunres2 5665	. . . . . . . 8
57	45, 46, 53, 56	syl3anc 1219	. . . . . . 7
58	55, 57	opeq12d 4149	. . . . . 6
59	44, 58	eqtr4d 2493	. . . . 5
60		reseq1 5186	. . . . . . 7
61		reseq1 5186	. . . . . . 7
62	60, 61	opeq12d 4149	. . . . . 6
63	62	eqeq2d 2463	. . . . 5
64	59, 63	syl5ibrcom 222	. . . 4
65		ffn 5641	. . . . . . . 8
66		fnresdm 5602	. . . . . . . 8
67	7, 65, 66	3syl 20	. . . . . . 7
68	67	ad2antrl 727	. . . . . 6
69	68	eqcomd 2457	. . . . 5
70		vex 3055	. . . . . . . . . 10
71	70	resex 5232	. . . . . . . . 9
72	70	resex 5232	. . . . . . . . 9
73	71, 72	op1std 6671	. . . . . . . 8
74	71, 72	op2ndd 6672	. . . . . . . 8
75	73, 74	uneq12d 3593	. . . . . . 7
76		resundi 5206	. . . . . . 7
77	75, 76	syl6eqr 2508	. . . . . 6
78	77	eqeq2d 2463	. . . . 5
79	69, 78	syl5ibrcom 222	. . . 4
80	64, 79	impbid 191	. . 3
81	80	ex 434	. 2
82	2, 6, 25, 42, 81	en3d 7430	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 965  =wceq 1370  e.wcel 1757  cvv 3052  u.cun 3408  i^icin 3409  C_wss 3410  c0 3719  <.cop 3965   class class class wbr 4374  X.cxp 4920  |`cres 4924  Fnwfn 5495  -->wf 5496  `cfv 5500  (class class class)co 6174  c1st 6659  c2nd 6660  cmap 7298  cen 7391

This theorem is referenced by:  map2xp  7565  mapdom2  7566  mapcdaen  8438  ackbij1lem5  8478  hashmap  12283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4174  df-iun 4255  df-br 4375  df-opab 4433  df-mpt 4434  df-id 4718  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-1st 6661  df-2nd 6662  df-map 7300  df-en 7395