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

Metamath Proof Explorer

Theorem xkohmeo

Description: The Exponential Law for topological spaces. The "currying" function F is a homeomorphism on function spaces when J and K are exponentiable spaces (by xkococn , it is sufficient to assume that J , K are locally compact to ensure exponentiability). (Contributed by Mario Carneiro, 13-Apr-2015) (Proof shortened by Mario Carneiro, 23-Aug-2015)

Ref Expression
Hypotheses xkohmeo.x 
|- ( ph -> J e. ( TopOn ` X ) )
xkohmeo.y 
|- ( ph -> K e. ( TopOn ` Y ) )
xkohmeo.f 
|- F = ( f e. ( ( J tX K ) Cn L ) |-> ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) )
xkohmeo.j 
|- ( ph -> J e. N-Locally Comp )
xkohmeo.k 
|- ( ph -> K e. N-Locally Comp )
xkohmeo.l 
|- ( ph -> L e. Top )
Assertion xkohmeo 
|- ( ph -> F e. ( ( L ^ko ( J tX K ) ) Homeo ( ( L ^ko K ) ^ko J ) ) )

Proof

Step Hyp Ref Expression
1 xkohmeo.x 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 xkohmeo.y 
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 xkohmeo.f 
 |-  F = ( f e. ( ( J tX K ) Cn L ) |-> ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) )
4 xkohmeo.j 
 |-  ( ph -> J e. N-Locally Comp )
5 xkohmeo.k 
 |-  ( ph -> K e. N-Locally Comp )
6 xkohmeo.l 
 |-  ( ph -> L e. Top )
7 txtopon 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
8 1 2 7 syl2anc 
 |-  ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
9 topontop 
 |-  ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) -> ( J tX K ) e. Top )
10 8 9 syl 
 |-  ( ph -> ( J tX K ) e. Top )
11 eqid 
 |-  ( L ^ko ( J tX K ) ) = ( L ^ko ( J tX K ) )
12 11 xkotopon 
 |-  ( ( ( J tX K ) e. Top /\ L e. Top ) -> ( L ^ko ( J tX K ) ) e. ( TopOn ` ( ( J tX K ) Cn L ) ) )
13 10 6 12 syl2anc 
 |-  ( ph -> ( L ^ko ( J tX K ) ) e. ( TopOn ` ( ( J tX K ) Cn L ) ) )
14 vex 
 |-  f e. _V
15 vex 
 |-  x e. _V
16 14 15 op1std 
 |-  ( z = <. f , x >. -> ( 1st ` z ) = f )
17 14 15 op2ndd 
 |-  ( z = <. f , x >. -> ( 2nd ` z ) = x )
18 eqidd 
 |-  ( z = <. f , x >. -> y = y )
19 16 17 18 oveq123d 
 |-  ( z = <. f , x >. -> ( ( 2nd ` z ) ( 1st ` z ) y ) = ( x f y ) )
20 19 mpteq2dv 
 |-  ( z = <. f , x >. -> ( y e. Y |-> ( ( 2nd ` z ) ( 1st ` z ) y ) ) = ( y e. Y |-> ( x f y ) ) )
21 20 mpompt 
 |-  ( z e. ( ( ( J tX K ) Cn L ) X. X ) |-> ( y e. Y |-> ( ( 2nd ` z ) ( 1st ` z ) y ) ) ) = ( f e. ( ( J tX K ) Cn L ) , x e. X |-> ( y e. Y |-> ( x f y ) ) )
22 txtopon 
 |-  ( ( ( L ^ko ( J tX K ) ) e. ( TopOn ` ( ( J tX K ) Cn L ) ) /\ J e. ( TopOn ` X ) ) -> ( ( L ^ko ( J tX K ) ) tX J ) e. ( TopOn ` ( ( ( J tX K ) Cn L ) X. X ) ) )
23 13 1 22 syl2anc 
 |-  ( ph -> ( ( L ^ko ( J tX K ) ) tX J ) e. ( TopOn ` ( ( ( J tX K ) Cn L ) X. X ) ) )
24 vex 
 |-  z e. _V
25 vex 
 |-  y e. _V
26 24 25 op1std 
 |-  ( w = <. z , y >. -> ( 1st ` w ) = z )
27 26 fveq2d 
 |-  ( w = <. z , y >. -> ( 1st ` ( 1st ` w ) ) = ( 1st ` z ) )
28 26 fveq2d 
 |-  ( w = <. z , y >. -> ( 2nd ` ( 1st ` w ) ) = ( 2nd ` z ) )
29 24 25 op2ndd 
 |-  ( w = <. z , y >. -> ( 2nd ` w ) = y )
30 27 28 29 oveq123d 
 |-  ( w = <. z , y >. -> ( ( 2nd ` ( 1st ` w ) ) ( 1st ` ( 1st ` w ) ) ( 2nd ` w ) ) = ( ( 2nd ` z ) ( 1st ` z ) y ) )
31 30 mpompt 
 |-  ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) |-> ( ( 2nd ` ( 1st ` w ) ) ( 1st ` ( 1st ` w ) ) ( 2nd ` w ) ) ) = ( z e. ( ( ( J tX K ) Cn L ) X. X ) , y e. Y |-> ( ( 2nd ` z ) ( 1st ` z ) y ) )
32 txtopon 
 |-  ( ( ( ( L ^ko ( J tX K ) ) tX J ) e. ( TopOn ` ( ( ( J tX K ) Cn L ) X. X ) ) /\ K e. ( TopOn ` Y ) ) -> ( ( ( L ^ko ( J tX K ) ) tX J ) tX K ) e. ( TopOn ` ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) ) )
33 23 2 32 syl2anc 
 |-  ( ph -> ( ( ( L ^ko ( J tX K ) ) tX J ) tX K ) e. ( TopOn ` ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) ) )
34 toptopon2 
 |-  ( L e. Top <-> L e. ( TopOn ` U. L ) )
35 6 34 sylib 
 |-  ( ph -> L e. ( TopOn ` U. L ) )
36 txcmp 
 |-  ( ( x e. Comp /\ y e. Comp ) -> ( x tX y ) e. Comp )
37 36 txnlly 
 |-  ( ( J e. N-Locally Comp /\ K e. N-Locally Comp ) -> ( J tX K ) e. N-Locally Comp )
38 4 5 37 syl2anc 
 |-  ( ph -> ( J tX K ) e. N-Locally Comp )
39 27 mpompt 
 |-  ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) |-> ( 1st ` ( 1st ` w ) ) ) = ( z e. ( ( ( J tX K ) Cn L ) X. X ) , y e. Y |-> ( 1st ` z ) )
40 8 adantr 
 |-  ( ( ph /\ w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
41 35 adantr 
 |-  ( ( ph /\ w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) ) -> L e. ( TopOn ` U. L ) )
42 xp1st 
 |-  ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) -> ( 1st ` w ) e. ( ( ( J tX K ) Cn L ) X. X ) )
43 42 adantl 
 |-  ( ( ph /\ w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) ) -> ( 1st ` w ) e. ( ( ( J tX K ) Cn L ) X. X ) )
44 xp1st 
 |-  ( ( 1st ` w ) e. ( ( ( J tX K ) Cn L ) X. X ) -> ( 1st ` ( 1st ` w ) ) e. ( ( J tX K ) Cn L ) )
45 43 44 syl 
 |-  ( ( ph /\ w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) ) -> ( 1st ` ( 1st ` w ) ) e. ( ( J tX K ) Cn L ) )
46 cnf2 
 |-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ L e. ( TopOn ` U. L ) /\ ( 1st ` ( 1st ` w ) ) e. ( ( J tX K ) Cn L ) ) -> ( 1st ` ( 1st ` w ) ) : ( X X. Y ) --> U. L )
47 40 41 45 46 syl3anc 
 |-  ( ( ph /\ w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) ) -> ( 1st ` ( 1st ` w ) ) : ( X X. Y ) --> U. L )
48 47 feqmptd 
 |-  ( ( ph /\ w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) ) -> ( 1st ` ( 1st ` w ) ) = ( u e. ( X X. Y ) |-> ( ( 1st ` ( 1st ` w ) ) ` u ) ) )
49 48 mpteq2dva 
 |-  ( ph -> ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) |-> ( 1st ` ( 1st ` w ) ) ) = ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) |-> ( u e. ( X X. Y ) |-> ( ( 1st ` ( 1st ` w ) ) ` u ) ) ) )
50 39 49 eqtr3id 
 |-  ( ph -> ( z e. ( ( ( J tX K ) Cn L ) X. X ) , y e. Y |-> ( 1st ` z ) ) = ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) |-> ( u e. ( X X. Y ) |-> ( ( 1st ` ( 1st ` w ) ) ` u ) ) ) )
51 23 2 cnmpt1st 
 |-  ( ph -> ( z e. ( ( ( J tX K ) Cn L ) X. X ) , y e. Y |-> z ) e. ( ( ( ( L ^ko ( J tX K ) ) tX J ) tX K ) Cn ( ( L ^ko ( J tX K ) ) tX J ) ) )
52 fveq2 
 |-  ( t = z -> ( 1st ` t ) = ( 1st ` z ) )
53 52 cbvmptv 
 |-  ( t e. ( ( ( J tX K ) Cn L ) X. X ) |-> ( 1st ` t ) ) = ( z e. ( ( ( J tX K ) Cn L ) X. X ) |-> ( 1st ` z ) )
54 16 mpompt 
 |-  ( z e. ( ( ( J tX K ) Cn L ) X. X ) |-> ( 1st ` z ) ) = ( f e. ( ( J tX K ) Cn L ) , x e. X |-> f )
55 13 1 cnmpt1st 
 |-  ( ph -> ( f e. ( ( J tX K ) Cn L ) , x e. X |-> f ) e. ( ( ( L ^ko ( J tX K ) ) tX J ) Cn ( L ^ko ( J tX K ) ) ) )
56 54 55 eqeltrid 
 |-  ( ph -> ( z e. ( ( ( J tX K ) Cn L ) X. X ) |-> ( 1st ` z ) ) e. ( ( ( L ^ko ( J tX K ) ) tX J ) Cn ( L ^ko ( J tX K ) ) ) )
57 53 56 eqeltrid 
 |-  ( ph -> ( t e. ( ( ( J tX K ) Cn L ) X. X ) |-> ( 1st ` t ) ) e. ( ( ( L ^ko ( J tX K ) ) tX J ) Cn ( L ^ko ( J tX K ) ) ) )
58 23 2 51 23 57 52 cnmpt21 
 |-  ( ph -> ( z e. ( ( ( J tX K ) Cn L ) X. X ) , y e. Y |-> ( 1st ` z ) ) e. ( ( ( ( L ^ko ( J tX K ) ) tX J ) tX K ) Cn ( L ^ko ( J tX K ) ) ) )
59 50 58 eqeltrrd 
 |-  ( ph -> ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) |-> ( u e. ( X X. Y ) |-> ( ( 1st ` ( 1st ` w ) ) ` u ) ) ) e. ( ( ( ( L ^ko ( J tX K ) ) tX J ) tX K ) Cn ( L ^ko ( J tX K ) ) ) )
60 28 mpompt 
 |-  ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) |-> ( 2nd ` ( 1st ` w ) ) ) = ( z e. ( ( ( J tX K ) Cn L ) X. X ) , y e. Y |-> ( 2nd ` z ) )
61 fveq2 
 |-  ( t = z -> ( 2nd ` t ) = ( 2nd ` z ) )
62 61 cbvmptv 
 |-  ( t e. ( ( ( J tX K ) Cn L ) X. X ) |-> ( 2nd ` t ) ) = ( z e. ( ( ( J tX K ) Cn L ) X. X ) |-> ( 2nd ` z ) )
63 17 mpompt 
 |-  ( z e. ( ( ( J tX K ) Cn L ) X. X ) |-> ( 2nd ` z ) ) = ( f e. ( ( J tX K ) Cn L ) , x e. X |-> x )
64 13 1 cnmpt2nd 
 |-  ( ph -> ( f e. ( ( J tX K ) Cn L ) , x e. X |-> x ) e. ( ( ( L ^ko ( J tX K ) ) tX J ) Cn J ) )
65 63 64 eqeltrid 
 |-  ( ph -> ( z e. ( ( ( J tX K ) Cn L ) X. X ) |-> ( 2nd ` z ) ) e. ( ( ( L ^ko ( J tX K ) ) tX J ) Cn J ) )
66 62 65 eqeltrid 
 |-  ( ph -> ( t e. ( ( ( J tX K ) Cn L ) X. X ) |-> ( 2nd ` t ) ) e. ( ( ( L ^ko ( J tX K ) ) tX J ) Cn J ) )
67 23 2 51 23 66 61 cnmpt21 
 |-  ( ph -> ( z e. ( ( ( J tX K ) Cn L ) X. X ) , y e. Y |-> ( 2nd ` z ) ) e. ( ( ( ( L ^ko ( J tX K ) ) tX J ) tX K ) Cn J ) )
68 60 67 eqeltrid 
 |-  ( ph -> ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) |-> ( 2nd ` ( 1st ` w ) ) ) e. ( ( ( ( L ^ko ( J tX K ) ) tX J ) tX K ) Cn J ) )
69 29 mpompt 
 |-  ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) |-> ( 2nd ` w ) ) = ( z e. ( ( ( J tX K ) Cn L ) X. X ) , y e. Y |-> y )
70 23 2 cnmpt2nd 
 |-  ( ph -> ( z e. ( ( ( J tX K ) Cn L ) X. X ) , y e. Y |-> y ) e. ( ( ( ( L ^ko ( J tX K ) ) tX J ) tX K ) Cn K ) )
71 69 70 eqeltrid 
 |-  ( ph -> ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) |-> ( 2nd ` w ) ) e. ( ( ( ( L ^ko ( J tX K ) ) tX J ) tX K ) Cn K ) )
72 33 68 71 cnmpt1t 
 |-  ( ph -> ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) |-> <. ( 2nd ` ( 1st ` w ) ) , ( 2nd ` w ) >. ) e. ( ( ( ( L ^ko ( J tX K ) ) tX J ) tX K ) Cn ( J tX K ) ) )
73 fveq2 
 |-  ( u = <. ( 2nd ` ( 1st ` w ) ) , ( 2nd ` w ) >. -> ( ( 1st ` ( 1st ` w ) ) ` u ) = ( ( 1st ` ( 1st ` w ) ) ` <. ( 2nd ` ( 1st ` w ) ) , ( 2nd ` w ) >. ) )
74 df-ov 
 |-  ( ( 2nd ` ( 1st ` w ) ) ( 1st ` ( 1st ` w ) ) ( 2nd ` w ) ) = ( ( 1st ` ( 1st ` w ) ) ` <. ( 2nd ` ( 1st ` w ) ) , ( 2nd ` w ) >. )
75 73 74 eqtr4di 
 |-  ( u = <. ( 2nd ` ( 1st ` w ) ) , ( 2nd ` w ) >. -> ( ( 1st ` ( 1st ` w ) ) ` u ) = ( ( 2nd ` ( 1st ` w ) ) ( 1st ` ( 1st ` w ) ) ( 2nd ` w ) ) )
76 33 8 35 38 59 72 75 cnmptk1p 
 |-  ( ph -> ( w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) |-> ( ( 2nd ` ( 1st ` w ) ) ( 1st ` ( 1st ` w ) ) ( 2nd ` w ) ) ) e. ( ( ( ( L ^ko ( J tX K ) ) tX J ) tX K ) Cn L ) )
77 31 76 eqeltrrid 
 |-  ( ph -> ( z e. ( ( ( J tX K ) Cn L ) X. X ) , y e. Y |-> ( ( 2nd ` z ) ( 1st ` z ) y ) ) e. ( ( ( ( L ^ko ( J tX K ) ) tX J ) tX K ) Cn L ) )
78 23 2 77 cnmpt2k 
 |-  ( ph -> ( z e. ( ( ( J tX K ) Cn L ) X. X ) |-> ( y e. Y |-> ( ( 2nd ` z ) ( 1st ` z ) y ) ) ) e. ( ( ( L ^ko ( J tX K ) ) tX J ) Cn ( L ^ko K ) ) )
79 21 78 eqeltrrid 
 |-  ( ph -> ( f e. ( ( J tX K ) Cn L ) , x e. X |-> ( y e. Y |-> ( x f y ) ) ) e. ( ( ( L ^ko ( J tX K ) ) tX J ) Cn ( L ^ko K ) ) )
80 13 1 79 cnmpt2k 
 |-  ( ph -> ( f e. ( ( J tX K ) Cn L ) |-> ( x e. X |-> ( y e. Y |-> ( x f y ) ) ) ) e. ( ( L ^ko ( J tX K ) ) Cn ( ( L ^ko K ) ^ko J ) ) )
81 3 80 eqeltrid 
 |-  ( ph -> F e. ( ( L ^ko ( J tX K ) ) Cn ( ( L ^ko K ) ^ko J ) ) )
82 1 2 3 4 5 6 xkocnv 
 |-  ( ph -> `' F = ( g e. ( J Cn ( L ^ko K ) ) |-> ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) ) )
83 15 25 op1std 
 |-  ( z = <. x , y >. -> ( 1st ` z ) = x )
84 83 fveq2d 
 |-  ( z = <. x , y >. -> ( g ` ( 1st ` z ) ) = ( g ` x ) )
85 15 25 op2ndd 
 |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )
86 84 85 fveq12d 
 |-  ( z = <. x , y >. -> ( ( g ` ( 1st ` z ) ) ` ( 2nd ` z ) ) = ( ( g ` x ) ` y ) )
87 86 mpompt 
 |-  ( z e. ( X X. Y ) |-> ( ( g ` ( 1st ` z ) ) ` ( 2nd ` z ) ) ) = ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) )
88 87 mpteq2i 
 |-  ( g e. ( J Cn ( L ^ko K ) ) |-> ( z e. ( X X. Y ) |-> ( ( g ` ( 1st ` z ) ) ` ( 2nd ` z ) ) ) ) = ( g e. ( J Cn ( L ^ko K ) ) |-> ( x e. X , y e. Y |-> ( ( g ` x ) ` y ) ) )
89 82 88 eqtr4di 
 |-  ( ph -> `' F = ( g e. ( J Cn ( L ^ko K ) ) |-> ( z e. ( X X. Y ) |-> ( ( g ` ( 1st ` z ) ) ` ( 2nd ` z ) ) ) ) )
90 nllytop 
 |-  ( J e. N-Locally Comp -> J e. Top )
91 4 90 syl 
 |-  ( ph -> J e. Top )
92 nllytop 
 |-  ( K e. N-Locally Comp -> K e. Top )
93 5 92 syl 
 |-  ( ph -> K e. Top )
94 xkotop 
 |-  ( ( K e. Top /\ L e. Top ) -> ( L ^ko K ) e. Top )
95 93 6 94 syl2anc 
 |-  ( ph -> ( L ^ko K ) e. Top )
96 eqid 
 |-  ( ( L ^ko K ) ^ko J ) = ( ( L ^ko K ) ^ko J )
97 96 xkotopon 
 |-  ( ( J e. Top /\ ( L ^ko K ) e. Top ) -> ( ( L ^ko K ) ^ko J ) e. ( TopOn ` ( J Cn ( L ^ko K ) ) ) )
98 91 95 97 syl2anc 
 |-  ( ph -> ( ( L ^ko K ) ^ko J ) e. ( TopOn ` ( J Cn ( L ^ko K ) ) ) )
99 vex 
 |-  g e. _V
100 99 24 op1std 
 |-  ( w = <. g , z >. -> ( 1st ` w ) = g )
101 99 24 op2ndd 
 |-  ( w = <. g , z >. -> ( 2nd ` w ) = z )
102 101 fveq2d 
 |-  ( w = <. g , z >. -> ( 1st ` ( 2nd ` w ) ) = ( 1st ` z ) )
103 100 102 fveq12d 
 |-  ( w = <. g , z >. -> ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) = ( g ` ( 1st ` z ) ) )
104 101 fveq2d 
 |-  ( w = <. g , z >. -> ( 2nd ` ( 2nd ` w ) ) = ( 2nd ` z ) )
105 103 104 fveq12d 
 |-  ( w = <. g , z >. -> ( ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) ` ( 2nd ` ( 2nd ` w ) ) ) = ( ( g ` ( 1st ` z ) ) ` ( 2nd ` z ) ) )
106 105 mpompt 
 |-  ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) ` ( 2nd ` ( 2nd ` w ) ) ) ) = ( g e. ( J Cn ( L ^ko K ) ) , z e. ( X X. Y ) |-> ( ( g ` ( 1st ` z ) ) ` ( 2nd ` z ) ) )
107 txtopon 
 |-  ( ( ( ( L ^ko K ) ^ko J ) e. ( TopOn ` ( J Cn ( L ^ko K ) ) ) /\ ( J tX K ) e. ( TopOn ` ( X X. Y ) ) ) -> ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) e. ( TopOn ` ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) ) )
108 98 8 107 syl2anc 
 |-  ( ph -> ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) e. ( TopOn ` ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) ) )
109 2 adantr 
 |-  ( ( ph /\ w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) ) -> K e. ( TopOn ` Y ) )
110 35 adantr 
 |-  ( ( ph /\ w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) ) -> L e. ( TopOn ` U. L ) )
111 eqid 
 |-  ( L ^ko K ) = ( L ^ko K )
112 111 xkotopon 
 |-  ( ( K e. Top /\ L e. Top ) -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
113 93 6 112 syl2anc 
 |-  ( ph -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
114 xp1st 
 |-  ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) -> ( 1st ` w ) e. ( J Cn ( L ^ko K ) ) )
115 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) /\ ( 1st ` w ) e. ( J Cn ( L ^ko K ) ) ) -> ( 1st ` w ) : X --> ( K Cn L ) )
116 1 113 114 115 syl2an3an 
 |-  ( ( ph /\ w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) ) -> ( 1st ` w ) : X --> ( K Cn L ) )
117 xp2nd 
 |-  ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) -> ( 2nd ` w ) e. ( X X. Y ) )
118 117 adantl 
 |-  ( ( ph /\ w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) ) -> ( 2nd ` w ) e. ( X X. Y ) )
119 xp1st 
 |-  ( ( 2nd ` w ) e. ( X X. Y ) -> ( 1st ` ( 2nd ` w ) ) e. X )
120 118 119 syl 
 |-  ( ( ph /\ w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) ) -> ( 1st ` ( 2nd ` w ) ) e. X )
121 116 120 ffvelcdmd 
 |-  ( ( ph /\ w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) ) -> ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) e. ( K Cn L ) )
122 cnf2 
 |-  ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` U. L ) /\ ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) e. ( K Cn L ) ) -> ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) : Y --> U. L )
123 109 110 121 122 syl3anc 
 |-  ( ( ph /\ w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) ) -> ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) : Y --> U. L )
124 123 feqmptd 
 |-  ( ( ph /\ w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) ) -> ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) = ( y e. Y |-> ( ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) ` y ) ) )
125 124 mpteq2dva 
 |-  ( ph -> ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) ) = ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( y e. Y |-> ( ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) ` y ) ) ) )
126 100 mpompt 
 |-  ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( 1st ` w ) ) = ( g e. ( J Cn ( L ^ko K ) ) , z e. ( X X. Y ) |-> g )
127 116 feqmptd 
 |-  ( ( ph /\ w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) ) -> ( 1st ` w ) = ( x e. X |-> ( ( 1st ` w ) ` x ) ) )
128 127 mpteq2dva 
 |-  ( ph -> ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( 1st ` w ) ) = ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( x e. X |-> ( ( 1st ` w ) ` x ) ) ) )
129 126 128 eqtr3id 
 |-  ( ph -> ( g e. ( J Cn ( L ^ko K ) ) , z e. ( X X. Y ) |-> g ) = ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( x e. X |-> ( ( 1st ` w ) ` x ) ) ) )
130 98 8 cnmpt1st 
 |-  ( ph -> ( g e. ( J Cn ( L ^ko K ) ) , z e. ( X X. Y ) |-> g ) e. ( ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) Cn ( ( L ^ko K ) ^ko J ) ) )
131 129 130 eqeltrrd 
 |-  ( ph -> ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( x e. X |-> ( ( 1st ` w ) ` x ) ) ) e. ( ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) Cn ( ( L ^ko K ) ^ko J ) ) )
132 102 mpompt 
 |-  ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( 1st ` ( 2nd ` w ) ) ) = ( g e. ( J Cn ( L ^ko K ) ) , z e. ( X X. Y ) |-> ( 1st ` z ) )
133 98 8 cnmpt2nd 
 |-  ( ph -> ( g e. ( J Cn ( L ^ko K ) ) , z e. ( X X. Y ) |-> z ) e. ( ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) Cn ( J tX K ) ) )
134 52 cbvmptv 
 |-  ( t e. ( X X. Y ) |-> ( 1st ` t ) ) = ( z e. ( X X. Y ) |-> ( 1st ` z ) )
135 83 mpompt 
 |-  ( z e. ( X X. Y ) |-> ( 1st ` z ) ) = ( x e. X , y e. Y |-> x )
136 1 2 cnmpt1st 
 |-  ( ph -> ( x e. X , y e. Y |-> x ) e. ( ( J tX K ) Cn J ) )
137 135 136 eqeltrid 
 |-  ( ph -> ( z e. ( X X. Y ) |-> ( 1st ` z ) ) e. ( ( J tX K ) Cn J ) )
138 134 137 eqeltrid 
 |-  ( ph -> ( t e. ( X X. Y ) |-> ( 1st ` t ) ) e. ( ( J tX K ) Cn J ) )
139 98 8 133 8 138 52 cnmpt21 
 |-  ( ph -> ( g e. ( J Cn ( L ^ko K ) ) , z e. ( X X. Y ) |-> ( 1st ` z ) ) e. ( ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) Cn J ) )
140 132 139 eqeltrid 
 |-  ( ph -> ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( 1st ` ( 2nd ` w ) ) ) e. ( ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) Cn J ) )
141 fveq2 
 |-  ( x = ( 1st ` ( 2nd ` w ) ) -> ( ( 1st ` w ) ` x ) = ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) )
142 108 1 113 4 131 140 141 cnmptk1p 
 |-  ( ph -> ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) ) e. ( ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) Cn ( L ^ko K ) ) )
143 125 142 eqeltrrd 
 |-  ( ph -> ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( y e. Y |-> ( ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) ` y ) ) ) e. ( ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) Cn ( L ^ko K ) ) )
144 104 mpompt 
 |-  ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( 2nd ` ( 2nd ` w ) ) ) = ( g e. ( J Cn ( L ^ko K ) ) , z e. ( X X. Y ) |-> ( 2nd ` z ) )
145 61 cbvmptv 
 |-  ( t e. ( X X. Y ) |-> ( 2nd ` t ) ) = ( z e. ( X X. Y ) |-> ( 2nd ` z ) )
146 85 mpompt 
 |-  ( z e. ( X X. Y ) |-> ( 2nd ` z ) ) = ( x e. X , y e. Y |-> y )
147 1 2 cnmpt2nd 
 |-  ( ph -> ( x e. X , y e. Y |-> y ) e. ( ( J tX K ) Cn K ) )
148 146 147 eqeltrid 
 |-  ( ph -> ( z e. ( X X. Y ) |-> ( 2nd ` z ) ) e. ( ( J tX K ) Cn K ) )
149 145 148 eqeltrid 
 |-  ( ph -> ( t e. ( X X. Y ) |-> ( 2nd ` t ) ) e. ( ( J tX K ) Cn K ) )
150 98 8 133 8 149 61 cnmpt21 
 |-  ( ph -> ( g e. ( J Cn ( L ^ko K ) ) , z e. ( X X. Y ) |-> ( 2nd ` z ) ) e. ( ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) Cn K ) )
151 144 150 eqeltrid 
 |-  ( ph -> ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( 2nd ` ( 2nd ` w ) ) ) e. ( ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) Cn K ) )
152 fveq2 
 |-  ( y = ( 2nd ` ( 2nd ` w ) ) -> ( ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) ` y ) = ( ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) ` ( 2nd ` ( 2nd ` w ) ) ) )
153 108 2 35 5 143 151 152 cnmptk1p 
 |-  ( ph -> ( w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) |-> ( ( ( 1st ` w ) ` ( 1st ` ( 2nd ` w ) ) ) ` ( 2nd ` ( 2nd ` w ) ) ) ) e. ( ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) Cn L ) )
154 106 153 eqeltrrid 
 |-  ( ph -> ( g e. ( J Cn ( L ^ko K ) ) , z e. ( X X. Y ) |-> ( ( g ` ( 1st ` z ) ) ` ( 2nd ` z ) ) ) e. ( ( ( ( L ^ko K ) ^ko J ) tX ( J tX K ) ) Cn L ) )
155 98 8 154 cnmpt2k 
 |-  ( ph -> ( g e. ( J Cn ( L ^ko K ) ) |-> ( z e. ( X X. Y ) |-> ( ( g ` ( 1st ` z ) ) ` ( 2nd ` z ) ) ) ) e. ( ( ( L ^ko K ) ^ko J ) Cn ( L ^ko ( J tX K ) ) ) )
156 89 155 eqeltrd 
 |-  ( ph -> `' F e. ( ( ( L ^ko K ) ^ko J ) Cn ( L ^ko ( J tX K ) ) ) )
157 ishmeo 
 |-  ( F e. ( ( L ^ko ( J tX K ) ) Homeo ( ( L ^ko K ) ^ko J ) ) <-> ( F e. ( ( L ^ko ( J tX K ) ) Cn ( ( L ^ko K ) ^ko J ) ) /\ `' F e. ( ( ( L ^ko K ) ^ko J ) Cn ( L ^ko ( J tX K ) ) ) ) )
158 81 156 157 sylanbrc 
 |-  ( ph -> F e. ( ( L ^ko ( J tX K ) ) Homeo ( ( L ^ko K ) ^ko J ) ) )