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