Step |
Hyp |
Ref |
Expression |
1 |
|
cnmptk1p.j |
|- ( ph -> J e. ( TopOn ` X ) ) |
2 |
|
cnmptk1p.k |
|- ( ph -> K e. ( TopOn ` Y ) ) |
3 |
|
cnmptk1p.l |
|- ( ph -> L e. ( TopOn ` Z ) ) |
4 |
|
cnmptk1p.n |
|- ( ph -> K e. N-Locally Comp ) |
5 |
|
cnmptk1p.a |
|- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) ) |
6 |
|
cnmptk1p.b |
|- ( ph -> ( x e. X |-> B ) e. ( J Cn K ) ) |
7 |
|
cnmptk1p.c |
|- ( y = B -> A = C ) |
8 |
|
eqid |
|- ( y e. Y |-> A ) = ( y e. Y |-> A ) |
9 |
|
cnf2 |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ ( x e. X |-> B ) e. ( J Cn K ) ) -> ( x e. X |-> B ) : X --> Y ) |
10 |
1 2 6 9
|
syl3anc |
|- ( ph -> ( x e. X |-> B ) : X --> Y ) |
11 |
10
|
fvmptelrn |
|- ( ( ph /\ x e. X ) -> B e. Y ) |
12 |
7
|
eleq1d |
|- ( y = B -> ( A e. Z <-> C e. Z ) ) |
13 |
2
|
adantr |
|- ( ( ph /\ x e. X ) -> K e. ( TopOn ` Y ) ) |
14 |
3
|
adantr |
|- ( ( ph /\ x e. X ) -> L e. ( TopOn ` Z ) ) |
15 |
|
nllytop |
|- ( K e. N-Locally Comp -> K e. Top ) |
16 |
4 15
|
syl |
|- ( ph -> K e. Top ) |
17 |
|
topontop |
|- ( L e. ( TopOn ` Z ) -> L e. Top ) |
18 |
3 17
|
syl |
|- ( ph -> L e. Top ) |
19 |
|
eqid |
|- ( L ^ko K ) = ( L ^ko K ) |
20 |
19
|
xkotopon |
|- ( ( K e. Top /\ L e. Top ) -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) ) |
21 |
16 18 20
|
syl2anc |
|- ( ph -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) ) |
22 |
|
cnf2 |
|- ( ( J e. ( TopOn ` X ) /\ ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) /\ ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) ) -> ( x e. X |-> ( y e. Y |-> A ) ) : X --> ( K Cn L ) ) |
23 |
1 21 5 22
|
syl3anc |
|- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) : X --> ( K Cn L ) ) |
24 |
23
|
fvmptelrn |
|- ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) e. ( K Cn L ) ) |
25 |
|
cnf2 |
|- ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` Z ) /\ ( y e. Y |-> A ) e. ( K Cn L ) ) -> ( y e. Y |-> A ) : Y --> Z ) |
26 |
13 14 24 25
|
syl3anc |
|- ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) : Y --> Z ) |
27 |
8
|
fmpt |
|- ( A. y e. Y A e. Z <-> ( y e. Y |-> A ) : Y --> Z ) |
28 |
26 27
|
sylibr |
|- ( ( ph /\ x e. X ) -> A. y e. Y A e. Z ) |
29 |
12 28 11
|
rspcdva |
|- ( ( ph /\ x e. X ) -> C e. Z ) |
30 |
8 7 11 29
|
fvmptd3 |
|- ( ( ph /\ x e. X ) -> ( ( y e. Y |-> A ) ` B ) = C ) |
31 |
30
|
mpteq2dva |
|- ( ph -> ( x e. X |-> ( ( y e. Y |-> A ) ` B ) ) = ( x e. X |-> C ) ) |
32 |
|
eqid |
|- ( K Cn L ) = ( K Cn L ) |
33 |
|
toponuni |
|- ( K e. ( TopOn ` Y ) -> Y = U. K ) |
34 |
2 33
|
syl |
|- ( ph -> Y = U. K ) |
35 |
|
mpoeq12 |
|- ( ( ( K Cn L ) = ( K Cn L ) /\ Y = U. K ) -> ( f e. ( K Cn L ) , z e. Y |-> ( f ` z ) ) = ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) ) |
36 |
32 34 35
|
sylancr |
|- ( ph -> ( f e. ( K Cn L ) , z e. Y |-> ( f ` z ) ) = ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) ) |
37 |
|
eqid |
|- U. K = U. K |
38 |
|
eqid |
|- ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) = ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) |
39 |
37 38
|
xkofvcn |
|- ( ( K e. N-Locally Comp /\ L e. Top ) -> ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) e. ( ( ( L ^ko K ) tX K ) Cn L ) ) |
40 |
4 18 39
|
syl2anc |
|- ( ph -> ( f e. ( K Cn L ) , z e. U. K |-> ( f ` z ) ) e. ( ( ( L ^ko K ) tX K ) Cn L ) ) |
41 |
36 40
|
eqeltrd |
|- ( ph -> ( f e. ( K Cn L ) , z e. Y |-> ( f ` z ) ) e. ( ( ( L ^ko K ) tX K ) Cn L ) ) |
42 |
|
fveq1 |
|- ( f = ( y e. Y |-> A ) -> ( f ` z ) = ( ( y e. Y |-> A ) ` z ) ) |
43 |
|
fveq2 |
|- ( z = B -> ( ( y e. Y |-> A ) ` z ) = ( ( y e. Y |-> A ) ` B ) ) |
44 |
42 43
|
sylan9eq |
|- ( ( f = ( y e. Y |-> A ) /\ z = B ) -> ( f ` z ) = ( ( y e. Y |-> A ) ` B ) ) |
45 |
1 5 6 21 2 41 44
|
cnmpt12 |
|- ( ph -> ( x e. X |-> ( ( y e. Y |-> A ) ` B ) ) e. ( J Cn L ) ) |
46 |
31 45
|
eqeltrrd |
|- ( ph -> ( x e. X |-> C ) e. ( J Cn L ) ) |