Metamath Proof Explorer

Theorem mapen

Description: Two set exponentiations are equinumerous when their bases and exponents are equinumerous. Theorem 6H(c) of Enderton p. 139. (Contributed by NM, 16-Dec-2003) (Proof shortened by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion mapen 
|- ( ( A ~~ B /\ C ~~ D ) -> ( A ^m C ) ~~ ( B ^m D ) )

Proof

Step Hyp Ref Expression
1 bren 
 |-  ( A ~~ B <-> E. f f : A -1-1-onto-> B )
2 bren 
 |-  ( C ~~ D <-> E. g g : C -1-1-onto-> D )
3 exdistrv 
 |-  ( E. f E. g ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) <-> ( E. f f : A -1-1-onto-> B /\ E. g g : C -1-1-onto-> D ) )
4 ovexd 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( A ^m C ) e. _V )
5 ovexd 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( B ^m D ) e. _V )
6 elmapi 
 |-  ( x e. ( A ^m C ) -> x : C --> A )
7 f1of 
 |-  ( f : A -1-1-onto-> B -> f : A --> B )
8 7 adantr 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> f : A --> B )
9 fco 
 |-  ( ( f : A --> B /\ x : C --> A ) -> ( f o. x ) : C --> B )
10 8 9 sylan 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ x : C --> A ) -> ( f o. x ) : C --> B )
11 f1ocnv 
 |-  ( g : C -1-1-onto-> D -> `' g : D -1-1-onto-> C )
12 11 adantl 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> `' g : D -1-1-onto-> C )
13 f1of 
 |-  ( `' g : D -1-1-onto-> C -> `' g : D --> C )
14 12 13 syl 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> `' g : D --> C )
15 14 adantr 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ x : C --> A ) -> `' g : D --> C )
16 10 15 fcod 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ x : C --> A ) -> ( ( f o. x ) o. `' g ) : D --> B )
17 16 ex 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( x : C --> A -> ( ( f o. x ) o. `' g ) : D --> B ) )
18 6 17 syl5 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( x e. ( A ^m C ) -> ( ( f o. x ) o. `' g ) : D --> B ) )
19 f1ofo 
 |-  ( f : A -1-1-onto-> B -> f : A -onto-> B )
20 19 adantr 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> f : A -onto-> B )
21 forn 
 |-  ( f : A -onto-> B -> ran f = B )
22 20 21 syl 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ran f = B )
23 vex 
 |-  f e. _V
24 23 rnex 
 |-  ran f e. _V
25 22 24 eqeltrrdi 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> B e. _V )
26 f1ofo 
 |-  ( g : C -1-1-onto-> D -> g : C -onto-> D )
27 26 adantl 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> g : C -onto-> D )
28 forn 
 |-  ( g : C -onto-> D -> ran g = D )
29 27 28 syl 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ran g = D )
30 vex 
 |-  g e. _V
31 30 rnex 
 |-  ran g e. _V
32 29 31 eqeltrrdi 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> D e. _V )
33 25 32 elmapd 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( ( ( f o. x ) o. `' g ) e. ( B ^m D ) <-> ( ( f o. x ) o. `' g ) : D --> B ) )
34 18 33 sylibrd 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( x e. ( A ^m C ) -> ( ( f o. x ) o. `' g ) e. ( B ^m D ) ) )
35 elmapi 
 |-  ( y e. ( B ^m D ) -> y : D --> B )
36 f1ocnv 
 |-  ( f : A -1-1-onto-> B -> `' f : B -1-1-onto-> A )
37 36 adantr 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> `' f : B -1-1-onto-> A )
38 f1of 
 |-  ( `' f : B -1-1-onto-> A -> `' f : B --> A )
39 37 38 syl 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> `' f : B --> A )
40 39 adantr 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ y : D --> B ) -> `' f : B --> A )
41 id 
 |-  ( y : D --> B -> y : D --> B )
42 f1of 
 |-  ( g : C -1-1-onto-> D -> g : C --> D )
43 42 adantl 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> g : C --> D )
44 fco 
 |-  ( ( y : D --> B /\ g : C --> D ) -> ( y o. g ) : C --> B )
45 41 43 44 syl2anr 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ y : D --> B ) -> ( y o. g ) : C --> B )
46 40 45 fcod 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ y : D --> B ) -> ( `' f o. ( y o. g ) ) : C --> A )
47 46 ex 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( y : D --> B -> ( `' f o. ( y o. g ) ) : C --> A ) )
48 35 47 syl5 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( y e. ( B ^m D ) -> ( `' f o. ( y o. g ) ) : C --> A ) )
49 f1odm 
 |-  ( f : A -1-1-onto-> B -> dom f = A )
50 49 adantr 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> dom f = A )
51 23 dmex 
 |-  dom f e. _V
52 50 51 eqeltrrdi 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> A e. _V )
53 f1odm 
 |-  ( g : C -1-1-onto-> D -> dom g = C )
54 53 adantl 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> dom g = C )
55 30 dmex 
 |-  dom g e. _V
56 54 55 eqeltrrdi 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> C e. _V )
57 52 56 elmapd 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( ( `' f o. ( y o. g ) ) e. ( A ^m C ) <-> ( `' f o. ( y o. g ) ) : C --> A ) )
58 48 57 sylibrd 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( y e. ( B ^m D ) -> ( `' f o. ( y o. g ) ) e. ( A ^m C ) ) )
59 coass 
 |-  ( ( f o. `' f ) o. ( y o. g ) ) = ( f o. ( `' f o. ( y o. g ) ) )
60 f1ococnv2 
 |-  ( f : A -1-1-onto-> B -> ( f o. `' f ) = ( _I |` B ) )
61 60 ad2antrr 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( f o. `' f ) = ( _I |` B ) )
62 61 coeq1d 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. `' f ) o. ( y o. g ) ) = ( ( _I |` B ) o. ( y o. g ) ) )
63 45 adantrl 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( y o. g ) : C --> B )
64 fcoi2 
 |-  ( ( y o. g ) : C --> B -> ( ( _I |` B ) o. ( y o. g ) ) = ( y o. g ) )
65 63 64 syl 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( _I |` B ) o. ( y o. g ) ) = ( y o. g ) )
66 62 65 eqtrd 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. `' f ) o. ( y o. g ) ) = ( y o. g ) )
67 59 66 eqtr3id 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( f o. ( `' f o. ( y o. g ) ) ) = ( y o. g ) )
68 67 eqeq2d 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) = ( f o. ( `' f o. ( y o. g ) ) ) <-> ( f o. x ) = ( y o. g ) ) )
69 coass 
 |-  ( ( ( f o. x ) o. `' g ) o. g ) = ( ( f o. x ) o. ( `' g o. g ) )
70 f1ococnv1 
 |-  ( g : C -1-1-onto-> D -> ( `' g o. g ) = ( _I |` C ) )
71 70 ad2antlr 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( `' g o. g ) = ( _I |` C ) )
72 71 coeq2d 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) o. ( `' g o. g ) ) = ( ( f o. x ) o. ( _I |` C ) ) )
73 10 adantrr 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( f o. x ) : C --> B )
74 fcoi1 
 |-  ( ( f o. x ) : C --> B -> ( ( f o. x ) o. ( _I |` C ) ) = ( f o. x ) )
75 73 74 syl 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) o. ( _I |` C ) ) = ( f o. x ) )
76 72 75 eqtrd 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) o. ( `' g o. g ) ) = ( f o. x ) )
77 69 76 eqtrid 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( ( f o. x ) o. `' g ) o. g ) = ( f o. x ) )
78 77 eqeq2d 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( y o. g ) = ( ( ( f o. x ) o. `' g ) o. g ) <-> ( y o. g ) = ( f o. x ) ) )
79 eqcom 
 |-  ( ( y o. g ) = ( f o. x ) <-> ( f o. x ) = ( y o. g ) )
80 78 79 bitrdi 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( y o. g ) = ( ( ( f o. x ) o. `' g ) o. g ) <-> ( f o. x ) = ( y o. g ) ) )
81 68 80 bitr4d 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) = ( f o. ( `' f o. ( y o. g ) ) ) <-> ( y o. g ) = ( ( ( f o. x ) o. `' g ) o. g ) ) )
82 f1of1 
 |-  ( f : A -1-1-onto-> B -> f : A -1-1-> B )
83 82 ad2antrr 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> f : A -1-1-> B )
84 simprl 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> x : C --> A )
85 46 adantrl 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( `' f o. ( y o. g ) ) : C --> A )
86 cocan1 
 |-  ( ( f : A -1-1-> B /\ x : C --> A /\ ( `' f o. ( y o. g ) ) : C --> A ) -> ( ( f o. x ) = ( f o. ( `' f o. ( y o. g ) ) ) <-> x = ( `' f o. ( y o. g ) ) ) )
87 83 84 85 86 syl3anc 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) = ( f o. ( `' f o. ( y o. g ) ) ) <-> x = ( `' f o. ( y o. g ) ) ) )
88 27 adantr 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> g : C -onto-> D )
89 ffn 
 |-  ( y : D --> B -> y Fn D )
90 89 ad2antll 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> y Fn D )
91 16 adantrr 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) o. `' g ) : D --> B )
92 91 ffnd 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( f o. x ) o. `' g ) Fn D )
93 cocan2 
 |-  ( ( g : C -onto-> D /\ y Fn D /\ ( ( f o. x ) o. `' g ) Fn D ) -> ( ( y o. g ) = ( ( ( f o. x ) o. `' g ) o. g ) <-> y = ( ( f o. x ) o. `' g ) ) )
94 88 90 92 93 syl3anc 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( ( y o. g ) = ( ( ( f o. x ) o. `' g ) o. g ) <-> y = ( ( f o. x ) o. `' g ) ) )
95 81 87 94 3bitr3d 
 |-  ( ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) /\ ( x : C --> A /\ y : D --> B ) ) -> ( x = ( `' f o. ( y o. g ) ) <-> y = ( ( f o. x ) o. `' g ) ) )
96 95 ex 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( ( x : C --> A /\ y : D --> B ) -> ( x = ( `' f o. ( y o. g ) ) <-> y = ( ( f o. x ) o. `' g ) ) ) )
97 6 35 96 syl2ani 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( ( x e. ( A ^m C ) /\ y e. ( B ^m D ) ) -> ( x = ( `' f o. ( y o. g ) ) <-> y = ( ( f o. x ) o. `' g ) ) ) )
98 4 5 34 58 97 en3d 
 |-  ( ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( A ^m C ) ~~ ( B ^m D ) )
99 98 exlimivv 
 |-  ( E. f E. g ( f : A -1-1-onto-> B /\ g : C -1-1-onto-> D ) -> ( A ^m C ) ~~ ( B ^m D ) )
100 3 99 sylbir 
 |-  ( ( E. f f : A -1-1-onto-> B /\ E. g g : C -1-1-onto-> D ) -> ( A ^m C ) ~~ ( B ^m D ) )
101 1 2 100 syl2anb 
 |-  ( ( A ~~ B /\ C ~~ D ) -> ( A ^m C ) ~~ ( B ^m D ) )