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 e. V /\ B e. W /\ C e. X ) /\ ( A i^i B ) = (/) ) -> ( C ^m ( A u. B ) ) ~~ ( ( C ^m A ) X. ( C ^m B ) ) )

Proof

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