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