Metamath Proof Explorer

Theorem cnmptkp

Description: The evaluation of the inner function in a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses cnmptk1.j 
|- ( ph -> J e. ( TopOn ` X ) )
cnmptk1.k 
|- ( ph -> K e. ( TopOn ` Y ) )
cnmptk1.l 
|- ( ph -> L e. ( TopOn ` Z ) )
cnmptkp.a 
|- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )
cnmptkp.b 
|- ( ph -> B e. Y )
cnmptkp.c 
|- ( y = B -> A = C )
Assertion cnmptkp 
|- ( ph -> ( x e. X |-> C ) e. ( J Cn L ) )

Proof

Step Hyp Ref Expression
1 cnmptk1.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 cnmptk1.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 cnmptk1.l 
 |-  ( ph -> L e. ( TopOn ` Z ) )
4 cnmptkp.a 
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) )
5 cnmptkp.b 
 |-  ( ph -> B e. Y )
6 cnmptkp.c 
 |-  ( y = B -> A = C )
7 eqid 
 |-  ( y e. Y |-> A ) = ( y e. Y |-> A )
8 5 adantr 
 |-  ( ( ph /\ x e. X ) -> B e. Y )
9 6 eleq1d 
 |-  ( y = B -> ( A e. U. L <-> C e. U. L ) )
10 2 adantr 
 |-  ( ( ph /\ x e. X ) -> K e. ( TopOn ` Y ) )
11 topontop 
 |-  ( L e. ( TopOn ` Z ) -> L e. Top )
12 3 11 syl 
 |-  ( ph -> L e. Top )
13 12 adantr 
 |-  ( ( ph /\ x e. X ) -> L e. Top )
14 toptopon2 
 |-  ( L e. Top <-> L e. ( TopOn ` U. L ) )
15 13 14 sylib 
 |-  ( ( ph /\ x e. X ) -> L e. ( TopOn ` U. L ) )
16 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
17 2 16 syl 
 |-  ( ph -> K e. Top )
18 eqid 
 |-  ( L ^ko K ) = ( L ^ko K )
19 18 xkotopon 
 |-  ( ( K e. Top /\ L e. Top ) -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
20 17 12 19 syl2anc 
 |-  ( ph -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) )
21 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 ) )
22 1 20 4 21 syl3anc 
 |-  ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) : X --> ( K Cn L ) )
23 22 fvmptelcdm 
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) e. ( K Cn L ) )
24 cnf2 
 |-  ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` U. L ) /\ ( y e. Y |-> A ) e. ( K Cn L ) ) -> ( y e. Y |-> A ) : Y --> U. L )
25 10 15 23 24 syl3anc 
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) : Y --> U. L )
26 7 fmpt 
 |-  ( A. y e. Y A e. U. L <-> ( y e. Y |-> A ) : Y --> U. L )
27 25 26 sylibr 
 |-  ( ( ph /\ x e. X ) -> A. y e. Y A e. U. L )
28 9 27 8 rspcdva 
 |-  ( ( ph /\ x e. X ) -> C e. U. L )
29 7 6 8 28 fvmptd3 
 |-  ( ( ph /\ x e. X ) -> ( ( y e. Y |-> A ) ` B ) = C )
30 29 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( ( y e. Y |-> A ) ` B ) ) = ( x e. X |-> C ) )
31 toponuni 
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
32 2 31 syl 
 |-  ( ph -> Y = U. K )
33 5 32 eleqtrd 
 |-  ( ph -> B e. U. K )
34 eqid 
 |-  U. K = U. K
35 34 xkopjcn 
 |-  ( ( K e. Top /\ L e. Top /\ B e. U. K ) -> ( w e. ( K Cn L ) |-> ( w ` B ) ) e. ( ( L ^ko K ) Cn L ) )
36 17 12 33 35 syl3anc 
 |-  ( ph -> ( w e. ( K Cn L ) |-> ( w ` B ) ) e. ( ( L ^ko K ) Cn L ) )
37 fveq1 
 |-  ( w = ( y e. Y |-> A ) -> ( w ` B ) = ( ( y e. Y |-> A ) ` B ) )
38 1 4 20 36 37 cnmpt11 
 |-  ( ph -> ( x e. X |-> ( ( y e. Y |-> A ) ` B ) ) e. ( J Cn L ) )
39 30 38 eqeltrrd 
 |-  ( ph -> ( x e. X |-> C ) e. ( J Cn L ) )