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

Theorem mapxpen 7027
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
Dummy variables  f 
g  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovex 5883 . . 3  |-  ( ( A  ^m  B )  ^m  C )  e. 
_V
21a1i 10 . 2  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( ( A  ^m  B )  ^m  C
)  e.  _V )
3 ovex 5883 . . 3  |-  ( A  ^m  ( B  X.  C ) )  e. 
_V
43a1i 10 . 2  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( A  ^m  ( B  X.  C ) )  e.  _V )
5 elmapi 6792 . . . . . . . . . 10  |-  ( f  e.  ( ( A  ^m  B )  ^m  C )  ->  f : C --> ( A  ^m  B ) )
6 ffvelrn 5663 . . . . . . . . . 10  |-  ( ( f : C --> ( A  ^m  B )  /\  y  e.  C )  ->  ( f `  y
)  e.  ( A  ^m  B ) )
75, 6sylan 457 . . . . . . . . 9  |-  ( ( f  e.  ( ( A  ^m  B )  ^m  C )  /\  y  e.  C )  ->  ( f `  y
)  e.  ( A  ^m  B ) )
8 elmapi 6792 . . . . . . . . 9  |-  ( ( f `  y )  e.  ( A  ^m  B )  ->  (
f `  y ) : B --> A )
97, 8syl 15 . . . . . . . 8  |-  ( ( f  e.  ( ( A  ^m  B )  ^m  C )  /\  y  e.  C )  ->  ( f `  y
) : B --> A )
10 ffvelrn 5663 . . . . . . . 8  |-  ( ( ( f `  y
) : B --> A  /\  x  e.  B )  ->  ( ( f `  y ) `  x
)  e.  A )
119, 10sylan 457 . . . . . . 7  |-  ( ( ( f  e.  ( ( A  ^m  B
)  ^m  C )  /\  y  e.  C
)  /\  x  e.  B )  ->  (
( f `  y
) `  x )  e.  A )
1211an32s 779 . . . . . 6  |-  ( ( ( f  e.  ( ( A  ^m  B
)  ^m  C )  /\  x  e.  B
)  /\  y  e.  C )  ->  (
( f `  y
) `  x )  e.  A )
1312ralrimiva 2626 . . . . 5  |-  ( ( f  e.  ( ( A  ^m  B )  ^m  C )  /\  x  e.  B )  ->  A. y  e.  C  ( ( f `  y ) `  x
)  e.  A )
1413ralrimiva 2626 . . . 4  |-  ( f  e.  ( ( A  ^m  B )  ^m  C )  ->  A. x  e.  B  A. y  e.  C  ( (
f `  y ) `  x )  e.  A
)
15 eqid 2283 . . . . 5  |-  ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `
 x ) )  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )
1615fmpt2 6191 . . . 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 188 . . 3  |-  ( f  e.  ( ( A  ^m  B )  ^m  C )  ->  (
x  e.  B , 
y  e.  C  |->  ( ( f `  y
) `  x )
) : ( B  X.  C ) --> A )
18 simp1 955 . . . 4  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  A  e.  V )
19 xpexg 4800 . . . . 5  |-  ( ( B  e.  W  /\  C  e.  X )  ->  ( B  X.  C
)  e.  _V )
20193adant1 973 . . . 4  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  ( B  X.  C
)  e.  _V )
21 elmapg 6785 . . . 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 642 . . 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 212 . 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 6792 . . . . . . . . 9  |-  ( g  e.  ( A  ^m  ( B  X.  C
) )  ->  g : ( B  X.  C ) --> A )
2524adantl 452 . . . . . . . 8  |-  ( ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X
)  /\  g  e.  ( A  ^m  ( B  X.  C ) ) )  ->  g :
( B  X.  C
) --> A )
26 fovrn 5990 . . . . . . . . . 10  |-  ( ( g : ( B  X.  C ) --> A  /\  x  e.  B  /\  y  e.  C
)  ->  ( x
g y )  e.  A )
27263expa 1151 . . . . . . . . 9  |-  ( ( ( g : ( B  X.  C ) --> A  /\  x  e.  B )  /\  y  e.  C )  ->  (
x g y )  e.  A )
2827an32s 779 . . . . . . . 8  |-  ( ( ( g : ( B  X.  C ) --> A  /\  y  e.  C )  /\  x  e.  B )  ->  (
x g y )  e.  A )
2925, 28sylanl1 631 . . . . . . 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 2283 . . . . . . 7  |-  ( x  e.  B  |->  ( x g y ) )  =  ( x  e.  B  |->  ( x g y ) )
3129, 30fmptd 5684 . . . . . 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 6785 . . . . . . . 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 975 . . . . . . 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 706 . . . . . 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 223 . . . . 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 2283 . . . . 5  |-  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )
3735, 36fmptd 5684 . . . 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 423 . . 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 5883 . . . 4  |-  ( A  ^m  B )  e. 
_V
40 simp3 957 . . . 4  |-  ( ( A  e.  V  /\  B  e.  W  /\  C  e.  X )  ->  C  e.  X )
41 elmapg 6785 . . . 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 644 . . 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 225 . 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 5389 . . . . . . . . 9  |-  ( g : ( B  X.  C ) --> A  -> 
g  Fn  ( B  X.  C ) )
4524, 44syl 15 . . . . . . . 8  |-  ( g  e.  ( A  ^m  ( B  X.  C
) )  ->  g  Fn  ( B  X.  C
) )
4645ad2antll 709 . . . . . . 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 5952 . . . . . . 7  |-  ( g  Fn  ( B  X.  C )  <->  g  =  ( x  e.  B ,  y  e.  C  |->  ( x g y ) ) )
4846, 47sylib 188 . . . . . 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 957 . . . . . . . . . 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 700 . . . . . . . . . . . 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 974 . . . . . . . . . . 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 1049 . . . . . . . . . . 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 1048 . . . . . . . . . . 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 5401 . . . . . . . . . . 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 1182 . . . . . . . . . 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 5608 . . . . . . . . . 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 642 . . . . . . . . 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 5527 . . . . . . . 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 956 . . . . . . . . 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 5883 . . . . . . . . 9  |-  ( x g y )  e. 
_V
6130fvmpt2 5608 . . . . . . . . 9  |-  ( ( x  e.  B  /\  ( x g y )  e.  _V )  ->  ( ( x  e.  B  |->  ( x g y ) ) `  x )  =  ( x g y ) )
6259, 60, 61sylancl 643 . . . . . . . 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 2315 . . . . . . 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 5912 . . . . . 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 2318 . . . . 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 2283 . . . . . . 7  |-  B  =  B
67 nfcv 2419 . . . . . . . . . 10  |-  F/_ x C
68 nfmpt1 4109 . . . . . . . . . 10  |-  F/_ x
( x  e.  B  |->  ( x g y ) )
6967, 68nfmpt 4108 . . . . . . . . 9  |-  F/_ x
( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )
7069nfeq2 2430 . . . . . . . 8  |-  F/ x  f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )
71 nfmpt1 4109 . . . . . . . . . . . 12  |-  F/_ y
( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )
7271nfeq2 2430 . . . . . . . . . . 11  |-  F/ y  f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )
73 fveq1 5524 . . . . . . . . . . . . 13  |-  ( f  =  ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) )  ->  ( f `  y )  =  ( ( y  e.  C  |->  ( x  e.  B  |->  ( x g y ) ) ) `  y ) )
7473fveq1d 5527 . . . . . . . . . . . 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 22 . . . . . . . . . . 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 2624 . . . . . . . . . 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 2283 . . . . . . . . . 10  |-  C  =  C
7876, 77jctil 523 . . . . . . . . 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 22 . . . . . . . 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 2624 . . . . . . 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 5907 . . . . . . 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 644 . . . . . 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 2294 . . . . 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 213 . . . 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 708 . . . . . . 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 5575 . . . . . 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 732 . . . . . . . . 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 457 . . . . . . . 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 5575 . . . . . . 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 4106 . . . . . 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 2315 . . . . 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 5915 . . . . . . . . 9  |-  F/_ y
( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `  x
) )
9392nfeq2 2430 . . . . . . . 8  |-  F/ y  g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `
 x ) )
94 eqidd 2284 . . . . . . . . 9  |-  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  ->  B  =  B )
95 nfmpt21 5914 . . . . . . . . . . 11  |-  F/_ x
( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `  x
) )
9695nfeq2 2430 . . . . . . . . . 10  |-  F/ x  g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )
97 nfv 1605 . . . . . . . . . 10  |-  F/ x  y  e.  C
98 fvex 5539 . . . . . . . . . . . . 13  |-  ( ( f `  y ) `
 x )  e. 
_V
9915ovmpt4g 5970 . . . . . . . . . . . . 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 1266 . . . . . . . . . . . 12  |-  ( ( x  e.  B  /\  y  e.  C )  ->  ( x ( x  e.  B ,  y  e.  C  |->  ( ( f `  y ) `
 x ) ) y )  =  ( ( f `  y
) `  x )
)
101 oveq 5864 . . . . . . . . . . . . 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 2291 . . . . . . . . . . . 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 212 . . . . . . . . . . 11  |-  ( g  =  ( x  e.  B ,  y  e.  C  |->  ( ( f `
 y ) `  x ) )  -> 
( ( x  e.  B  /\  y  e.  C )  ->  (
x g y )  =  ( ( f `
 y ) `  x ) ) )
104103exp3acom23 1362 . . . . . . . . . 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 2631 . . . . . . . . 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 4099 . . . . . . . . 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 1353 . . . . . . . 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 2624 . . . . . . 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 4099 . . . . . . 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 644 . . . . . 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 2294 . . . . 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 213 . . . 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 183 . . 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 423 . 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 6898 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 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   A.wral 2543   _Vcvv 2788   class class class wbr 4023    e. cmpt 4077    X. cxp 4687    Fn wfn 5250   -->wf 5251   ` cfv 5255  (class class class)co 5858    e. cmpt2 5860    ^m cmap 6772    ~~ cen 6860
This theorem is referenced by:  mappwen  7739  cfpwsdom  8206  rpnnen  12505  rexpen  12506
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-map 6774  df-en 6864
  Copyright terms: Public domain W3C validator