This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mapxpen

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)

Ref Expression
Assertion mapxpen 
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A ^m B ) ^m C ) ~~ ( A ^m ( B X. C ) ) )

Proof

Step Hyp Ref Expression
1 ovexd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A ^m B ) ^m C ) e. _V )
2 ovexd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A ^m ( B X. C ) ) e. _V )
3 elmapi 
 |-  ( f e. ( ( A ^m B ) ^m C ) -> f : C --> ( A ^m B ) )
4 3 ffvelcdmda 
 |-  ( ( f e. ( ( A ^m B ) ^m C ) /\ y e. C ) -> ( f ` y ) e. ( A ^m B ) )
5 elmapi 
 |-  ( ( f ` y ) e. ( A ^m B ) -> ( f ` y ) : B --> A )
6 4 5 syl 
 |-  ( ( f e. ( ( A ^m B ) ^m C ) /\ y e. C ) -> ( f ` y ) : B --> A )
7 6 ffvelcdmda 
 |-  ( ( ( f e. ( ( A ^m B ) ^m C ) /\ y e. C ) /\ x e. B ) -> ( ( f ` y ) ` x ) e. A )
8 7 an32s 
 |-  ( ( ( f e. ( ( A ^m B ) ^m C ) /\ x e. B ) /\ y e. C ) -> ( ( f ` y ) ` x ) e. A )
9 8 ralrimiva 
 |-  ( ( f e. ( ( A ^m B ) ^m C ) /\ x e. B ) -> A. y e. C ( ( f ` y ) ` x ) e. A )
10 9 ralrimiva 
 |-  ( f e. ( ( A ^m B ) ^m C ) -> A. x e. B A. y e. C ( ( f ` y ) ` x ) e. A )
11 eqid 
 |-  ( x e. B , y e. C |-> ( ( f ` y ) ` x ) ) = ( x e. B , y e. C |-> ( ( f ` y ) ` x ) )
12 11 fmpo 
 |-  ( 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 )
13 10 12 sylib 
 |-  ( f e. ( ( A ^m B ) ^m C ) -> ( x e. B , y e. C |-> ( ( f ` y ) ` x ) ) : ( B X. C ) --> A )
14 simp1 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> A e. V )
15 xpexg 
 |-  ( ( B e. W /\ C e. X ) -> ( B X. C ) e. _V )
16 15 3adant1 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( B X. C ) e. _V )
17 elmapg 
 |-  ( ( 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 ) )
18 14 16 17 syl2anc 
 |-  ( ( 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 ) )
19 13 18 imbitrrid 
 |-  ( ( 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 ) ) ) )
20 elmapi 
 |-  ( g e. ( A ^m ( B X. C ) ) -> g : ( B X. C ) --> A )
21 20 adantl 
 |-  ( ( ( A e. V /\ B e. W /\ C e. X ) /\ g e. ( A ^m ( B X. C ) ) ) -> g : ( B X. C ) --> A )
22 fovcdm 
 |-  ( ( g : ( B X. C ) --> A /\ x e. B /\ y e. C ) -> ( x g y ) e. A )
23 22 3expa 
 |-  ( ( ( g : ( B X. C ) --> A /\ x e. B ) /\ y e. C ) -> ( x g y ) e. A )
24 23 an32s 
 |-  ( ( ( g : ( B X. C ) --> A /\ y e. C ) /\ x e. B ) -> ( x g y ) e. A )
25 21 24 sylanl1 
 |-  ( ( ( ( ( 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 )
26 25 fmpttd 
 |-  ( ( ( ( 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 )
27 elmapg 
 |-  ( ( A e. V /\ B e. W ) -> ( ( x e. B |-> ( x g y ) ) e. ( A ^m B ) <-> ( x e. B |-> ( x g y ) ) : B --> A ) )
28 27 3adant3 
 |-  ( ( 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 ) )
29 28 ad2antrr 
 |-  ( ( ( ( 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 ) )
30 26 29 mpbird 
 |-  ( ( ( ( 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 ) )
31 30 fmpttd 
 |-  ( ( ( 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 ) )
32 31 ex 
 |-  ( ( 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 ) ) )
33 ovex 
 |-  ( A ^m B ) e. _V
34 simp3 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> C e. X )
35 elmapg 
 |-  ( ( ( 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 ) ) )
36 33 34 35 sylancr 
 |-  ( ( 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 ) ) )
37 32 36 sylibrd 
 |-  ( ( 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 ) ) )
38 elmapfn 
 |-  ( g e. ( A ^m ( B X. C ) ) -> g Fn ( B X. C ) )
39 38 ad2antll 
 |-  ( ( ( 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 ) )
40 fnov 
 |-  ( g Fn ( B X. C ) <-> g = ( x e. B , y e. C |-> ( x g y ) ) )
41 39 40 sylib 
 |-  ( ( ( 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 ) ) )
42 simp3 
 |-  ( ( ( ( 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 )
43 26 adantlrl 
 |-  ( ( ( ( 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 )
44 43 3adant2 
 |-  ( ( ( ( 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 )
45 simp1l2 
 |-  ( ( ( ( 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 )
46 simp1l1 
 |-  ( ( ( ( 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 )
47 fex2 
 |-  ( ( ( x e. B |-> ( x g y ) ) : B --> A /\ B e. W /\ A e. V ) -> ( x e. B |-> ( x g y ) ) e. _V )
48 44 45 46 47 syl3anc 
 |-  ( ( ( ( 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 )
49 eqid 
 |-  ( y e. C |-> ( x e. B |-> ( x g y ) ) ) = ( y e. C |-> ( x e. B |-> ( x g y ) ) )
50 49 fvmpt2 
 |-  ( ( 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 ) ) )
51 42 48 50 syl2anc 
 |-  ( ( ( ( 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 ) ) )
52 51 fveq1d 
 |-  ( ( ( ( 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 ) )
53 simp2 
 |-  ( ( ( ( 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 )
54 ovex 
 |-  ( x g y ) e. _V
55 eqid 
 |-  ( x e. B |-> ( x g y ) ) = ( x e. B |-> ( x g y ) )
56 55 fvmpt2 
 |-  ( ( x e. B /\ ( x g y ) e. _V ) -> ( ( x e. B |-> ( x g y ) ) ` x ) = ( x g y ) )
57 53 54 56 sylancl 
 |-  ( ( ( ( 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 ) )
58 52 57 eqtrd 
 |-  ( ( ( ( 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 ) )
59 58 mpoeq3dva 
 |-  ( ( ( 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 ) ) )
60 41 59 eqtr4d 
 |-  ( ( ( 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 ) ) )
61 eqid 
 |-  B = B
62 nfcv 
 |-  F/_ x C
63 nfmpt1 
 |-  F/_ x ( x e. B |-> ( x g y ) )
64 62 63 nfmpt 
 |-  F/_ x ( y e. C |-> ( x e. B |-> ( x g y ) ) )
65 64 nfeq2 
 |-  F/ x f = ( y e. C |-> ( x e. B |-> ( x g y ) ) )
66 nfmpt1 
 |-  F/_ y ( y e. C |-> ( x e. B |-> ( x g y ) ) )
67 66 nfeq2 
 |-  F/ y f = ( y e. C |-> ( x e. B |-> ( x g y ) ) )
68 fveq1 
 |-  ( f = ( y e. C |-> ( x e. B |-> ( x g y ) ) ) -> ( f ` y ) = ( ( y e. C |-> ( x e. B |-> ( x g y ) ) ) ` y ) )
69 68 fveq1d 
 |-  ( f = ( y e. C |-> ( x e. B |-> ( x g y ) ) ) -> ( ( f ` y ) ` x ) = ( ( ( y e. C |-> ( x e. B |-> ( x g y ) ) ) ` y ) ` x ) )
70 69 a1d 
 |-  ( 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 ) ) )
71 67 70 ralrimi 
 |-  ( 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 ) )
72 eqid 
 |-  C = C
73 71 72 jctil 
 |-  ( 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 ) ) )
74 73 a1d 
 |-  ( 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 ) ) ) )
75 65 74 ralrimi 
 |-  ( 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 ) ) )
76 mpoeq123 
 |-  ( ( 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 ) ) )
77 61 75 76 sylancr 
 |-  ( 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 ) ) )
78 77 eqeq2d 
 |-  ( 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 ) ) ) )
79 60 78 syl5ibrcom 
 |-  ( ( ( 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 ) ) ) )
80 3 ad2antrl 
 |-  ( ( ( 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 ) )
81 80 feqmptd 
 |-  ( ( ( 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 ) ) )
82 simprl 
 |-  ( ( ( 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 ) )
83 82 6 sylan 
 |-  ( ( ( ( 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 )
84 83 feqmptd 
 |-  ( ( ( ( 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 ) ) )
85 84 mpteq2dva 
 |-  ( ( ( 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 ) ) ) )
86 81 85 eqtrd 
 |-  ( ( ( 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 ) ) ) )
87 nfmpo2 
 |-  F/_ y ( x e. B , y e. C |-> ( ( f ` y ) ` x ) )
88 87 nfeq2 
 |-  F/ y g = ( x e. B , y e. C |-> ( ( f ` y ) ` x ) )
89 eqidd 
 |-  ( g = ( x e. B , y e. C |-> ( ( f ` y ) ` x ) ) -> B = B )
90 nfmpo1 
 |-  F/_ x ( x e. B , y e. C |-> ( ( f ` y ) ` x ) )
91 90 nfeq2 
 |-  F/ x g = ( x e. B , y e. C |-> ( ( f ` y ) ` x ) )
92 nfv 
 |-  F/ x y e. C
93 fvex 
 |-  ( ( f ` y ) ` x ) e. _V
94 11 ovmpt4g 
 |-  ( ( 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 ) )
95 93 94 mp3an3 
 |-  ( ( x e. B /\ y e. C ) -> ( x ( x e. B , y e. C |-> ( ( f ` y ) ` x ) ) y ) = ( ( f ` y ) ` x ) )
96 oveq 
 |-  ( g = ( x e. B , y e. C |-> ( ( f ` y ) ` x ) ) -> ( x g y ) = ( x ( x e. B , y e. C |-> ( ( f ` y ) ` x ) ) y ) )
97 96 eqeq1d 
 |-  ( 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 ) ) )
98 95 97 imbitrrid 
 |-  ( g = ( x e. B , y e. C |-> ( ( f ` y ) ` x ) ) -> ( ( x e. B /\ y e. C ) -> ( x g y ) = ( ( f ` y ) ` x ) ) )
99 98 expcomd 
 |-  ( g = ( x e. B , y e. C |-> ( ( f ` y ) ` x ) ) -> ( y e. C -> ( x e. B -> ( x g y ) = ( ( f ` y ) ` x ) ) ) )
100 91 92 99 ralrimd 
 |-  ( g = ( x e. B , y e. C |-> ( ( f ` y ) ` x ) ) -> ( y e. C -> A. x e. B ( x g y ) = ( ( f ` y ) ` x ) ) )
101 mpteq12 
 |-  ( ( B = B /\ A. x e. B ( x g y ) = ( ( f ` y ) ` x ) ) -> ( x e. B |-> ( x g y ) ) = ( x e. B |-> ( ( f ` y ) ` x ) ) )
102 89 100 101 syl6an 
 |-  ( 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 ) ) ) )
103 88 102 ralrimi 
 |-  ( 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 ) ) )
104 mpteq12 
 |-  ( ( 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 ) ) ) )
105 72 103 104 sylancr 
 |-  ( 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 ) ) ) )
106 105 eqeq2d 
 |-  ( 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 ) ) ) ) )
107 86 106 syl5ibrcom 
 |-  ( ( ( 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 ) ) ) ) )
108 79 107 impbid 
 |-  ( ( ( 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 ) ) ) )
109 108 ex 
 |-  ( ( 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 ) ) ) ) )
110 1 2 19 37 109 en3d 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A ^m B ) ^m C ) ~~ ( A ^m ( B X. C ) ) )