Metamath Proof Explorer


Theorem mapunen

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
Assertion mapunen A V B W C X A B = C A B C A × C B

Proof

Step Hyp Ref Expression
1 ovexd A V B W C X A B = C A B V
2 ovexd A V B W C X A B = C A V
3 ovexd A V B W C X A B = C B V
4 2 3 xpexd A V B W C X A B = C A × C B V
5 elmapi x C A B x : A B C
6 ssun1 A A B
7 fssres x : A B C A A B x A : A C
8 5 6 7 sylancl x C A B x A : A C
9 ssun2 B A B
10 fssres x : A B C B A B x B : B C
11 5 9 10 sylancl x C A B x B : B C
12 8 11 jca x C A B x A : A C x B : B C
13 opelxp x A x B C A × C B x A C A x B C B
14 simpl3 A V B W C X A B = C X
15 simpl1 A V B W C X A B = A V
16 14 15 elmapd A V B W C X A B = x A C A x A : A C
17 simpl2 A V B W C X A B = B W
18 14 17 elmapd A V B W C X A B = x B C B x B : B C
19 16 18 anbi12d A V B W C X A B = x A C A x B C B x A : A C x B : B C
20 13 19 bitrid A V B W C X A B = x A x B C A × C B x A : A C x B : B C
21 12 20 syl5ibr A V B W C X A B = x C A B x A x B C A × C B
22 xp1st y C A × C B 1 st y C A
23 22 adantl A V B W C X A B = y C A × C B 1 st y C A
24 elmapi 1 st y C A 1 st y : A C
25 23 24 syl A V B W C X A B = y C A × C B 1 st y : A C
26 xp2nd y C A × C B 2 nd y C B
27 26 adantl A V B W C X A B = y C A × C B 2 nd y C B
28 elmapi 2 nd y C B 2 nd y : B C
29 27 28 syl A V B W C X A B = y C A × C B 2 nd y : B C
30 simplr A V B W C X A B = y C A × C B A B =
31 25 29 30 fun2d A V B W C X A B = y C A × C B 1 st y 2 nd y : A B C
32 31 ex A V B W C X A B = y C A × C B 1 st y 2 nd y : A B C
33 unexg A V B W A B V
34 15 17 33 syl2anc A V B W C X A B = A B V
35 14 34 elmapd A V B W C X A B = 1 st y 2 nd y C A B 1 st y 2 nd y : A B C
36 32 35 sylibrd A V B W C X A B = y C A × C B 1 st y 2 nd y C A B
37 1st2nd2 y C A × C B y = 1 st y 2 nd y
38 37 ad2antll A V B W C X A B = x C A B y C A × C B y = 1 st y 2 nd y
39 25 adantrl A V B W C X A B = x C A B y C A × C B 1 st y : A C
40 29 adantrl A V B W C X A B = x C A B y C A × C B 2 nd y : B C
41 res0 1 st y =
42 res0 2 nd y =
43 41 42 eqtr4i 1 st y = 2 nd y
44 simplr A V B W C X A B = x C A B y C A × C B A B =
45 44 reseq2d A V B W C X A B = x C A B y C A × C B 1 st y A B = 1 st y
46 44 reseq2d A V B W C X A B = x C A B y C A × C B 2 nd y A B = 2 nd y
47 43 45 46 3eqtr4a A V B W C X A B = x C A B y C A × C B 1 st y A B = 2 nd y A B
48 fresaunres1 1 st y : A C 2 nd y : B C 1 st y A B = 2 nd y A B 1 st y 2 nd y A = 1 st y
49 39 40 47 48 syl3anc A V B W C X A B = x C A B y C A × C B 1 st y 2 nd y A = 1 st y
50 fresaunres2 1 st y : A C 2 nd y : B C 1 st y A B = 2 nd y A B 1 st y 2 nd y B = 2 nd y
51 39 40 47 50 syl3anc A V B W C X A B = x C A B y C A × C B 1 st y 2 nd y B = 2 nd y
52 49 51 opeq12d A V B W C X A B = x C A B y C A × C B 1 st y 2 nd y A 1 st y 2 nd y B = 1 st y 2 nd y
53 38 52 eqtr4d A V B W C X A B = x C A B y C A × C B y = 1 st y 2 nd y A 1 st y 2 nd y B
54 reseq1 x = 1 st y 2 nd y x A = 1 st y 2 nd y A
55 reseq1 x = 1 st y 2 nd y x B = 1 st y 2 nd y B
56 54 55 opeq12d x = 1 st y 2 nd y x A x B = 1 st y 2 nd y A 1 st y 2 nd y B
57 56 eqeq2d x = 1 st y 2 nd y y = x A x B y = 1 st y 2 nd y A 1 st y 2 nd y B
58 53 57 syl5ibrcom A V B W C X A B = x C A B y C A × C B x = 1 st y 2 nd y y = x A x B
59 ffn x : A B C x Fn A B
60 fnresdm x Fn A B x A B = x
61 5 59 60 3syl x C A B x A B = x
62 61 ad2antrl A V B W C X A B = x C A B y C A × C B x A B = x
63 62 eqcomd A V B W C X A B = x C A B y C A × C B x = x A B
64 vex x V
65 64 resex x A V
66 64 resex x B V
67 65 66 op1std y = x A x B 1 st y = x A
68 65 66 op2ndd y = x A x B 2 nd y = x B
69 67 68 uneq12d y = x A x B 1 st y 2 nd y = x A x B
70 resundi x A B = x A x B
71 69 70 eqtr4di y = x A x B 1 st y 2 nd y = x A B
72 71 eqeq2d y = x A x B x = 1 st y 2 nd y x = x A B
73 63 72 syl5ibrcom A V B W C X A B = x C A B y C A × C B y = x A x B x = 1 st y 2 nd y
74 58 73 impbid A V B W C X A B = x C A B y C A × C B x = 1 st y 2 nd y y = x A x B
75 74 ex A V B W C X A B = x C A B y C A × C B x = 1 st y 2 nd y y = x A x B
76 1 4 21 36 75 en3d A V B W C X A B = C A B C A × C B