![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > mapunen | Unicode version |
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.) |
Ref | Expression |
---|---|
mapunen |
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 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 <-> wb 184
/\ wa 369 /\ w3a 965 = wceq 1370
e. wcel 1757 cvv 3052
u. cun 3408 i^i cin 3409 C_ wss 3410
c0 3719 <. cop 3965 class class class wbr 4374
X. cxp 4920 |` cres 4924 Fn wfn 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 |
Copyright terms: Public domain | W3C validator |