# 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 ) )`
` |-  ( ( ph /\ w e. ( ( ( ( J tX K ) Cn L ) X. X ) X. Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 syl5eqr
` |-  ( 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 ) ) ) )`
` |-  ( ( ph /\ w e. ( ( J Cn ( L ^ko K ) ) X. ( X X. Y ) ) ) -> K e. ( TopOn ` Y ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 syl5eqr
` |-  ( 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 ) ) )`