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 ffvelrnd
 |-  ( ( 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 ) ) )