MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mapxpen Unicode version

Theorem mapxpen 6995
Description: Equinumerosity law for double set exponentiation. Proposition 10.45 of [TakeutiZaring] p. 96. (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2015.)
Assertion
Ref Expression
mapxpen  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( ( A  ^m  B )  ^m  C
)  ~~  ( A  ^m  ( B  X.  C
) ) )

Proof of Theorem mapxpen
StepHypRef Expression
1 ovex 5817 . . 3  |-  ( ( A  ^m  B )  ^m  C )  e. 
_V
21a1i 12 . 2  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( ( A  ^m  B )  ^m  C
)  e.  _V )
3 ovex 5817 . . 3  |-  ( A  ^m  ( B  X.  C ) )  e. 
_V
43a1i 12 . 2  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( A  ^m  ( B  X.  C ) )  e.  _V )
5 elmapi 6760 . . . . . . . . . 10  |-  ( f  e.  ( ( A  ^m  B )  ^m  C )  ->  f : C --> ( A  ^m  B ) )
6 ffvelrn 5597 . . . . . . . . . 10  |-  ( ( f : C --> ( A  ^m  B )  /\  y  e.  C )  ->  ( f `  y
)  e.  ( A  ^m  B ) )
75, 6sylan 459 . . . . . . . . 9  |-  ( ( f  e.  ( ( A  ^m  B )  ^m  C )  /\  y  e.  C )  ->  ( f `  y
)  e.  ( A  ^m  B ) )
8 elmapi 6760 . . . . . . . . 9  |-  ( ( f `  y )  e.  ( A  ^m  B )  ->  (
f `  y ) : B --> A )
97, 8syl 17 . . . . . . . 8  |-  ( ( f  e.  ( ( A  ^m  B )  ^m  C )  /\  y  e.  C )  ->  ( f `  y
) : B --> A )
10 ffvelrn 5597 . . . . . . . 8  |-  ( ( ( f `  y
) : B --> A  /\  x  e.  B )  ->  ( ( f `  y ) `  x
)  e.  A )
119, 10sylan 459 . . . . . . 7  |-  ( ( ( f  e.  ( ( A  ^m  B
)  ^m  C )  /\  y  e.  C
)  /\  x  e.  B )  ->  (
( f `  y
) `  x )  e.  A )
1211an32s 782 . . . . . 6  |-  ( ( ( f  e.  ( ( A  ^m  B
)  ^m  C )  /\  x  e.  B
)  /\  y  e.  C )  ->  (
( f `  y
) `  x )  e.  A )
1312ralrimiva 2601 . . . . 5  |-  ( ( f  e.  ( ( A  ^m  B )  ^m  C )  /\  x  e.  B )  ->  A. y  e.  C  ( ( f `  y ) `  x
)  e.  A )
1413ralrimiva 2601 . . . 4  |-  ( f  e.  ( ( A  ^m  B )  ^m  C )  ->  A. x  e.  B  A. y  e.  C  ( (
f `  y ) `  x )  e.  A
)
15 eqid 2258 . . . . 5  |-  ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `
 x ) )  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )
1615fmpt2 6125 . . . 4  |-  ( A. x  e.  B  A. y  e.  C  (
( f `  y
) `  x )  e.  A  <->  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) ) : ( B  X.  C
) --> A )
1714, 16sylib 190 . . 3  |-  ( f  e.  ( ( A  ^m  B )  ^m  C )  ->  (
x  e.  B , 
y  e.  C  |->  ( ( f `  y
) `  x )
) : ( B  X.  C ) --> A )
18 simp1 960 . . . 4  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  A  e.  V )
19 xpexg 4788 . . . . 5  |-  ( ( B  e.  W  /\  C  e.  X )  ->  ( B  X.  C
)  e.  _V )
20193adant1 978 . . . 4  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( B  X.  C
)  e.  _V )
21 elmapg 6753 . . . 4  |-  ( ( A  e.  V  /\  ( B  X.  C
)  e.  _V )  ->  ( ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  e.  ( A  ^m  ( B  X.  C ) )  <-> 
( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `  x
) ) : ( B  X.  C ) --> A ) )
2218, 20, 21syl2anc 645 . . 3  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  e.  ( A  ^m  ( B  X.  C ) )  <-> 
( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `  x
) ) : ( B  X.  C ) --> A ) )
2317, 22syl5ibr 214 . 2  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( f  e.  ( ( A  ^m  B
)  ^m  C )  ->  ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `  x
) )  e.  ( A  ^m  ( B  X.  C ) ) ) )
24 elmapi 6760 . . . . . . . . 9  |-  ( g  e.  ( A  ^m  ( B  X.  C
) )  ->  g : ( B  X.  C ) --> A )
2524adantl 454 . . . . . . . 8  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) )  ->  g :
( B  X.  C
) --> A )
26 fovrn 5924 . . . . . . . . . 10  |-  ( ( g : ( B  X.  C ) --> A  /\  x  e.  B  /\  y  e.  C
)  ->  ( x
g y )  e.  A )
27263expa 1156 . . . . . . . . 9  |-  ( ( ( g : ( B  X.  C ) --> A  /\  x  e.  B )  /\  y  e.  C )  ->  (
x g y )  e.  A )
2827an32s 782 . . . . . . . 8  |-  ( ( ( g : ( B  X.  C ) --> A  /\  y  e.  C )  /\  x  e.  B )  ->  (
x g y )  e.  A )
2925, 28sylanl1 634 . . . . . . 7  |-  ( ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  g  e.  ( A  ^m  ( B  X.  C ) ) )  /\  y  e.  C )  /\  x  e.  B )  ->  (
x g y )  e.  A )
30 eqid 2258 . . . . . . 7  |-  ( x  e.  B  |->  ( x g y ) )  =  ( x  e.  B  |->  ( x g y ) )
3129, 30fmptd 5618 . . . . . 6  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  g  e.  ( A  ^m  ( B  X.  C ) ) )  /\  y  e.  C )  ->  (
x  e.  B  |->  ( x g y ) ) : B --> A )
32 elmapg 6753 . . . . . . . 8  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( ( x  e.  B  |->  ( x g y ) )  e.  ( A  ^m  B
)  <->  ( x  e.  B  |->  ( x g y ) ) : B --> A ) )
33323adant3 980 . . . . . . 7  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( ( x  e.  B  |->  ( x g y ) )  e.  ( A  ^m  B
)  <->  ( x  e.  B  |->  ( x g y ) ) : B --> A ) )
3433ad2antrr 709 . . . . . 6  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  g  e.  ( A  ^m  ( B  X.  C ) ) )  /\  y  e.  C )  ->  (
( x  e.  B  |->  ( x g y ) )  e.  ( A  ^m  B )  <-> 
( x  e.  B  |->  ( x g y ) ) : B --> A ) )
3531, 34mpbird 225 . . . . 5  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  g  e.  ( A  ^m  ( B  X.  C ) ) )  /\  y  e.  C )  ->  (
x  e.  B  |->  ( x g y ) )  e.  ( A  ^m  B ) )
36 eqid 2258 . . . . 5  |-  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )
3735, 36fmptd 5618 . . . 4  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) )  ->  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) : C --> ( A  ^m  B ) )
3837ex 425 . . 3  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( g  e.  ( A  ^m  ( B  X.  C ) )  ->  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) : C --> ( A  ^m  B ) ) )
39 ovex 5817 . . . 4  |-  ( A  ^m  B )  e. 
_V
40 simp3 962 . . . 4  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  C  e.  X )
41 elmapg 6753 . . . 4  |-  ( ( ( A  ^m  B
)  e.  _V  /\  C  e.  X )  ->  ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  e.  ( ( A  ^m  B )  ^m  C )  <->  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) : C --> ( A  ^m  B ) ) )
4239, 40, 41sylancr 647 . . 3  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  e.  ( ( A  ^m  B )  ^m  C )  <->  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) : C --> ( A  ^m  B ) ) )
4338, 42sylibrd 227 . 2  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( g  e.  ( A  ^m  ( B  X.  C ) )  ->  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  e.  ( ( A  ^m  B )  ^m  C ) ) )
44 ffn 5327 . . . . . . . . 9  |-  ( g : ( B  X.  C ) --> A  -> 
g  Fn  ( B  X.  C ) )
4524, 44syl 17 . . . . . . . 8  |-  ( g  e.  ( A  ^m  ( B  X.  C
) )  ->  g  Fn  ( B  X.  C
) )
4645ad2antll 712 . . . . . . 7  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) ) )  ->  g  Fn  ( B  X.  C
) )
47 fnov 5886 . . . . . . 7  |-  ( g  Fn  ( B  X.  C )  <->  g  =  ( x  e.  B ,  y  e.  C  |->  ( x g y ) ) )
4846, 47sylib 190 . . . . . 6  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) ) )  ->  g  =  ( x  e.  B ,  y  e.  C  |->  ( x g y ) ) )
49 simp3 962 . . . . . . . . . 10  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  x  e.  B  /\  y  e.  C
)  ->  y  e.  C )
5031adantlrl 703 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  y  e.  C
)  ->  ( x  e.  B  |->  ( x g y ) ) : B --> A )
51503adant2 979 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  x  e.  B  /\  y  e.  C
)  ->  ( x  e.  B  |->  ( x g y ) ) : B --> A )
52 simp1l2 1054 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  x  e.  B  /\  y  e.  C
)  ->  B  e.  W )
53 simp1l1 1053 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  x  e.  B  /\  y  e.  C
)  ->  A  e.  V )
54 fex2 5339 . . . . . . . . . . 11  |-  ( ( ( x  e.  B  |->  ( x g y ) ) : B --> A  /\  B  e.  W  /\  A  e.  V
)  ->  ( x  e.  B  |->  ( x g y ) )  e.  _V )
5551, 52, 53, 54syl3anc 1187 . . . . . . . . . 10  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  x  e.  B  /\  y  e.  C
)  ->  ( x  e.  B  |->  ( x g y ) )  e.  _V )
5636fvmpt2 5542 . . . . . . . . . 10  |-  ( ( y  e.  C  /\  ( x  e.  B  |->  ( x g y ) )  e.  _V )  ->  ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y )  =  ( x  e.  B  |->  ( x g y ) ) )
5749, 55, 56syl2anc 645 . . . . . . . . 9  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  x  e.  B  /\  y  e.  C
)  ->  ( (
y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y
)  =  ( x  e.  B  |->  ( x g y ) ) )
5857fveq1d 5460 . . . . . . . 8  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  x  e.  B  /\  y  e.  C
)  ->  ( (
( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y ) `  x
)  =  ( ( x  e.  B  |->  ( x g y ) ) `  x ) )
59 simp2 961 . . . . . . . . 9  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  x  e.  B  /\  y  e.  C
)  ->  x  e.  B )
60 ovex 5817 . . . . . . . . 9  |-  ( x g y )  e. 
_V
6130fvmpt2 5542 . . . . . . . . 9  |-  ( ( x  e.  B  /\  ( x g y )  e.  _V )  ->  ( ( x  e.  B  |->  ( x g y ) ) `  x )  =  ( x g y ) )
6259, 60, 61sylancl 646 . . . . . . . 8  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  x  e.  B  /\  y  e.  C
)  ->  ( (
x  e.  B  |->  ( x g y ) ) `  x )  =  ( x g y ) )
6358, 62eqtrd 2290 . . . . . . 7  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  x  e.  B  /\  y  e.  C
)  ->  ( (
( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y ) `  x
)  =  ( x g y ) )
6463mpt2eq3dva 5846 . . . . . 6  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) ) )  ->  (
x  e.  B , 
y  e.  C  |->  ( ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `
 y ) `  x ) )  =  ( x  e.  B ,  y  e.  C  |->  ( x g y ) ) )
6548, 64eqtr4d 2293 . . . . 5  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) ) )  ->  g  =  ( x  e.  B ,  y  e.  C  |->  ( ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y
) `  x )
) )
66 eqid 2258 . . . . . . 7  |-  B  =  B
67 nfcv 2394 . . . . . . . . . 10  |-  F/_ x C
68 nfmpt1 4083 . . . . . . . . . 10  |-  F/_ x
( x  e.  B  |->  ( x g y ) )
6967, 68nfmpt 4082 . . . . . . . . 9  |-  F/_ x
( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )
7069nfeq2 2405 . . . . . . . 8  |-  F/ x  f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )
71 nfmpt1 4083 . . . . . . . . . . . 12  |-  F/_ y
( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )
7271nfeq2 2405 . . . . . . . . . . 11  |-  F/ y  f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )
73 fveq1 5457 . . . . . . . . . . . . 13  |-  ( f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  ->  ( f `  y )  =  ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y ) )
7473fveq1d 5460 . . . . . . . . . . . 12  |-  ( f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  ->  ( ( f `
 y ) `  x )  =  ( ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `
 y ) `  x ) )
7574a1d 24 . . . . . . . . . . 11  |-  ( f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  ->  ( y  e.  C  ->  ( (
f `  y ) `  x )  =  ( ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `
 y ) `  x ) ) )
7672, 75ralrimi 2599 . . . . . . . . . 10  |-  ( f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  ->  A. y  e.  C  ( ( f `  y ) `  x
)  =  ( ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y ) `  x
) )
77 eqid 2258 . . . . . . . . . 10  |-  C  =  C
7876, 77jctil 525 . . . . . . . . 9  |-  ( f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  ->  ( C  =  C  /\  A. y  e.  C  ( (
f `  y ) `  x )  =  ( ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `
 y ) `  x ) ) )
7978a1d 24 . . . . . . . 8  |-  ( f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  ->  ( x  e.  B  ->  ( C  =  C  /\  A. y  e.  C  ( (
f `  y ) `  x )  =  ( ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `
 y ) `  x ) ) ) )
8070, 79ralrimi 2599 . . . . . . 7  |-  ( f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  ->  A. x  e.  B  ( C  =  C  /\  A. y  e.  C  ( ( f `  y ) `  x
)  =  ( ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y ) `  x
) ) )
81 mpt2eq123 5841 . . . . . . 7  |-  ( ( B  =  B  /\  A. x  e.  B  ( C  =  C  /\  A. y  e.  C  ( ( f `  y
) `  x )  =  ( ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y
) `  x )
) )  ->  (
x  e.  B , 
y  e.  C  |->  ( ( f `  y
) `  x )
)  =  ( x  e.  B ,  y  e.  C  |->  ( ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y ) `  x
) ) )
8266, 80, 81sylancr 647 . . . . . 6  |-  ( f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  ->  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  =  ( x  e.  B ,  y  e.  C  |->  ( ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y ) `
 x ) ) )
8382eqeq2d 2269 . . . . 5  |-  ( f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  ->  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `  x
) )  <->  g  =  ( x  e.  B ,  y  e.  C  |->  ( ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y ) `
 x ) ) ) )
8465, 83syl5ibrcom 215 . . . 4  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) ) )  ->  (
f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  ->  g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `  x
) ) ) )
855ad2antrl 711 . . . . . . 7  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) ) )  ->  f : C --> ( A  ^m  B ) )
8685feqmptd 5509 . . . . . 6  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) ) )  ->  f  =  ( y  e.  C  |->  ( f `  y ) ) )
87 simprl 735 . . . . . . . . 9  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) ) )  ->  f  e.  ( ( A  ^m  B )  ^m  C
) )
8887, 9sylan 459 . . . . . . . 8  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  y  e.  C
)  ->  ( f `  y ) : B --> A )
8988feqmptd 5509 . . . . . . 7  |-  ( ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  /\  (
f  e.  ( ( A  ^m  B )  ^m  C )  /\  g  e.  ( A  ^m  ( B  X.  C
) ) ) )  /\  y  e.  C
)  ->  ( f `  y )  =  ( x  e.  B  |->  ( ( f `  y
) `  x )
) )
9089mpteq2dva 4080 . . . . . 6  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) ) )  ->  (
y  e.  C  |->  ( f `  y ) )  =  ( y  e.  C  |->  ( x  e.  B  |->  ( ( f `  y ) `
 x ) ) ) )
9186, 90eqtrd 2290 . . . . 5  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) ) )  ->  f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( ( f `
 y ) `  x ) ) ) )
92 nfmpt22 5849 . . . . . . . . 9  |-  F/_ y
( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `  x
) )
9392nfeq2 2405 . . . . . . . 8  |-  F/ y  g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `
 x ) )
94 eqidd 2259 . . . . . . . . 9  |-  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  ->  B  =  B )
95 nfmpt21 5848 . . . . . . . . . . 11  |-  F/_ x
( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `  x
) )
9695nfeq2 2405 . . . . . . . . . 10  |-  F/ x  g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )
97 nfv 1629 . . . . . . . . . 10  |-  F/ x  y  e.  C
98 fvex 5472 . . . . . . . . . . . . 13  |-  ( ( f `  y ) `
 x )  e. 
_V
9915ovmpt4g 5904 . . . . . . . . . . . . 13  |-  ( ( x  e.  B  /\  y  e.  C  /\  ( ( f `  y ) `  x
)  e.  _V )  ->  ( x ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `
 x ) ) y )  =  ( ( f `  y
) `  x )
)
10098, 99mp3an3 1271 . . . . . . . . . . . 12  |-  ( ( x  e.  B  /\  y  e.  C )  ->  ( x ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `
 x ) ) y )  =  ( ( f `  y
) `  x )
)
101 oveq 5798 . . . . . . . . . . . . 13  |-  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  -> 
( x g y )  =  ( x ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `  x
) ) y ) )
102101eqeq1d 2266 . . . . . . . . . . . 12  |-  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  -> 
( ( x g y )  =  ( ( f `  y
) `  x )  <->  ( x ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) ) y )  =  ( ( f `  y ) `
 x ) ) )
103100, 102syl5ibr 214 . . . . . . . . . . 11  |-  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  -> 
( ( x  e.  B  /\  y  e.  C )  ->  (
x g y )  =  ( ( f `
 y ) `  x ) ) )
104103exp3acom23 1368 . . . . . . . . . 10  |-  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  -> 
( y  e.  C  ->  ( x  e.  B  ->  ( x g y )  =  ( ( f `  y ) `
 x ) ) ) )
10596, 97, 104ralrimd 2606 . . . . . . . . 9  |-  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  -> 
( y  e.  C  ->  A. x  e.  B  ( x g y )  =  ( ( f `  y ) `
 x ) ) )
106 mpteq12 4073 . . . . . . . . 9  |-  ( ( B  =  B  /\  A. x  e.  B  ( x g y )  =  ( ( f `
 y ) `  x ) )  -> 
( x  e.  B  |->  ( x g y ) )  =  ( x  e.  B  |->  ( ( f `  y
) `  x )
) )
10794, 105, 106ee12an 1359 . . . . . . . 8  |-  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  -> 
( y  e.  C  ->  ( x  e.  B  |->  ( x g y ) )  =  ( x  e.  B  |->  ( ( f `  y
) `  x )
) ) )
10893, 107ralrimi 2599 . . . . . . 7  |-  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  ->  A. y  e.  C  ( x  e.  B  |->  ( x g y ) )  =  ( x  e.  B  |->  ( ( f `  y
) `  x )
) )
109 mpteq12 4073 . . . . . . 7  |-  ( ( C  =  C  /\  A. y  e.  C  ( x  e.  B  |->  ( x g y ) )  =  ( x  e.  B  |->  ( ( f `  y ) `
 x ) ) )  ->  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  =  ( y  e.  C  |->  ( x  e.  B  |->  ( ( f `  y ) `
 x ) ) ) )
11077, 108, 109sylancr 647 . . . . . 6  |-  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  -> 
( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  =  ( y  e.  C  |->  ( x  e.  B  |->  ( ( f `  y ) `  x
) ) ) )
111110eqeq2d 2269 . . . . 5  |-  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  -> 
( f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  <->  f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( ( f `  y ) `  x
) ) ) ) )
11291, 111syl5ibrcom 215 . . . 4  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) ) )  ->  (
g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `
 x ) )  ->  f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) ) )
11384, 112impbid 185 . . 3  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) ) )  ->  (
f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  <->  g  =  ( x  e.  B , 
y  e.  C  |->  ( ( f `  y
) `  x )
) ) )
114113ex 425 . 2  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( ( f  e.  ( ( A  ^m  B )  ^m  C
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) )  ->  ( f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  <-> 
g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `
 x ) ) ) ) )
1152, 4, 23, 43, 114en3d 6866 1  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( ( A  ^m  B )  ^m  C
)  ~~  ( A  ^m  ( B  X.  C
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    /\ w3a 939    = wceq 1619    e. wcel 1621   A.wral 2518   _Vcvv 2763   class class class wbr 3997    e. cmpt 4051    X. cxp 4659    Fn wfn 4668   -->wf 4669   ` cfv 4673  (class class class)co 5792    e. cmpt2 5794    ^m cmap 6740    ~~ cen 6828
This theorem is referenced by:  mappwen  7707  cfpwsdom  8174  rpnnen  12468  rexpen  12469
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pow 4160  ax-pr 4186  ax-un 4484
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-sbc 2967  df-csb 3057  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-pw 3601  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-iun 3881  df-br 3998  df-opab 4052  df-mpt 4053  df-id 4281  df-xp 4675  df-rel 4676  df-cnv 4677  df-co 4678  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fun 4683  df-fn 4684  df-f 4685  df-f1 4686  df-fo 4687  df-f1o 4688  df-fv 4689  df-ov 5795  df-oprab 5796  df-mpt2 5797  df-1st 6056  df-2nd 6057  df-map 6742  df-en 6832
  Copyright terms: Public domain W3C validator