MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnmpt21 Structured version   Unicode version

Theorem cnmpt21 20673
Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
cnmpt21.j  |-  ( ph  ->  J  e.  (TopOn `  X ) )
cnmpt21.k  |-  ( ph  ->  K  e.  (TopOn `  Y ) )
cnmpt21.a  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  A )  e.  ( ( J  tX  K
)  Cn  L ) )
cnmpt21.l  |-  ( ph  ->  L  e.  (TopOn `  Z ) )
cnmpt21.b  |-  ( ph  ->  ( z  e.  Z  |->  B )  e.  ( L  Cn  M ) )
cnmpt21.c  |-  ( z  =  A  ->  B  =  C )
Assertion
Ref Expression
cnmpt21  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  C )  e.  ( ( J  tX  K
)  Cn  M ) )
Distinct variable groups:    z, A    z, J    x, y, z, L    ph, x, y, z   
x, X, y, z   
x, M, y, z   
x, Y, y, z   
z, K    x, Z, y, z    x, B, y   
z, C
Allowed substitution hints:    A( x, y)    B( z)    C( x, y)    J( x, y)    K( x, y)

Proof of Theorem cnmpt21
Dummy variables  u  v  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ov 6305 . . . . . . . . . 10  |-  ( x ( x  e.  X ,  y  e.  Y  |->  A ) y )  =  ( ( x  e.  X ,  y  e.  Y  |->  A ) `
 <. x ,  y
>. )
2 simprl 762 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  ->  x  e.  X )
3 simprr 764 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  -> 
y  e.  Y )
4 cnmpt21.j . . . . . . . . . . . . . . . 16  |-  ( ph  ->  J  e.  (TopOn `  X ) )
5 cnmpt21.k . . . . . . . . . . . . . . . 16  |-  ( ph  ->  K  e.  (TopOn `  Y ) )
6 txtopon 20593 . . . . . . . . . . . . . . . 16  |-  ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  ->  ( J  tX  K )  e.  (TopOn `  ( X  X.  Y
) ) )
74, 5, 6syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( J  tX  K
)  e.  (TopOn `  ( X  X.  Y
) ) )
8 cnmpt21.l . . . . . . . . . . . . . . 15  |-  ( ph  ->  L  e.  (TopOn `  Z ) )
9 cnmpt21.a . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  A )  e.  ( ( J  tX  K
)  Cn  L ) )
10 cnf2 20252 . . . . . . . . . . . . . . 15  |-  ( ( ( J  tX  K
)  e.  (TopOn `  ( X  X.  Y
) )  /\  L  e.  (TopOn `  Z )  /\  ( x  e.  X ,  y  e.  Y  |->  A )  e.  ( ( J  tX  K
)  Cn  L ) )  ->  ( x  e.  X ,  y  e.  Y  |->  A ) : ( X  X.  Y
) --> Z )
117, 8, 9, 10syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  A ) : ( X  X.  Y ) --> Z )
12 eqid 2422 . . . . . . . . . . . . . . 15  |-  ( x  e.  X ,  y  e.  Y  |->  A )  =  ( x  e.  X ,  y  e.  Y  |->  A )
1312fmpt2 6871 . . . . . . . . . . . . . 14  |-  ( A. x  e.  X  A. y  e.  Y  A  e.  Z  <->  ( x  e.  X ,  y  e.  Y  |->  A ) : ( X  X.  Y
) --> Z )
1411, 13sylibr 215 . . . . . . . . . . . . 13  |-  ( ph  ->  A. x  e.  X  A. y  e.  Y  A  e.  Z )
15 rsp2 2799 . . . . . . . . . . . . 13  |-  ( A. x  e.  X  A. y  e.  Y  A  e.  Z  ->  ( ( x  e.  X  /\  y  e.  Y )  ->  A  e.  Z ) )
1614, 15syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( x  e.  X  /\  y  e.  Y )  ->  A  e.  Z ) )
1716imp 430 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  ->  A  e.  Z )
1812ovmpt4g 6430 . . . . . . . . . . 11  |-  ( ( x  e.  X  /\  y  e.  Y  /\  A  e.  Z )  ->  ( x ( x  e.  X ,  y  e.  Y  |->  A ) y )  =  A )
192, 3, 17, 18syl3anc 1264 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  -> 
( x ( x  e.  X ,  y  e.  Y  |->  A ) y )  =  A )
201, 19syl5eqr 2477 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  -> 
( ( x  e.  X ,  y  e.  Y  |->  A ) `  <. x ,  y >.
)  =  A )
2120fveq2d 5882 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  -> 
( ( z  e.  Z  |->  B ) `  ( ( x  e.  X ,  y  e.  Y  |->  A ) `  <. x ,  y >.
) )  =  ( ( z  e.  Z  |->  B ) `  A
) )
22 cnmpt21.b . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( z  e.  Z  |->  B )  e.  ( L  Cn  M ) )
23 cntop2 20244 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  Z  |->  B )  e.  ( L  Cn  M )  ->  M  e.  Top )
2422, 23syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  Top )
25 eqid 2422 . . . . . . . . . . . . . . 15  |-  U. M  =  U. M
2625toptopon 19935 . . . . . . . . . . . . . 14  |-  ( M  e.  Top  <->  M  e.  (TopOn `  U. M ) )
2724, 26sylib 199 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  (TopOn `  U. M ) )
28 cnf2 20252 . . . . . . . . . . . . 13  |-  ( ( L  e.  (TopOn `  Z )  /\  M  e.  (TopOn `  U. M )  /\  ( z  e.  Z  |->  B )  e.  ( L  Cn  M
) )  ->  (
z  e.  Z  |->  B ) : Z --> U. M
)
298, 27, 22, 28syl3anc 1264 . . . . . . . . . . . 12  |-  ( ph  ->  ( z  e.  Z  |->  B ) : Z --> U. M )
30 eqid 2422 . . . . . . . . . . . . 13  |-  ( z  e.  Z  |->  B )  =  ( z  e.  Z  |->  B )
3130fmpt 6055 . . . . . . . . . . . 12  |-  ( A. z  e.  Z  B  e.  U. M  <->  ( z  e.  Z  |->  B ) : Z --> U. M
)
3229, 31sylibr 215 . . . . . . . . . . 11  |-  ( ph  ->  A. z  e.  Z  B  e.  U. M )
3332adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  ->  A. z  e.  Z  B  e.  U. M )
34 cnmpt21.c . . . . . . . . . . . 12  |-  ( z  =  A  ->  B  =  C )
3534eleq1d 2491 . . . . . . . . . . 11  |-  ( z  =  A  ->  ( B  e.  U. M  <->  C  e.  U. M ) )
3635rspcv 3178 . . . . . . . . . 10  |-  ( A  e.  Z  ->  ( A. z  e.  Z  B  e.  U. M  ->  C  e.  U. M ) )
3717, 33, 36sylc 62 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  ->  C  e.  U. M )
3834, 30fvmptg 5959 . . . . . . . . 9  |-  ( ( A  e.  Z  /\  C  e.  U. M )  ->  ( ( z  e.  Z  |->  B ) `
 A )  =  C )
3917, 37, 38syl2anc 665 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  -> 
( ( z  e.  Z  |->  B ) `  A )  =  C )
4021, 39eqtrd 2463 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  -> 
( ( z  e.  Z  |->  B ) `  ( ( x  e.  X ,  y  e.  Y  |->  A ) `  <. x ,  y >.
) )  =  C )
41 opelxpi 4882 . . . . . . . 8  |-  ( ( x  e.  X  /\  y  e.  Y )  -> 
<. x ,  y >.  e.  ( X  X.  Y
) )
42 fvco3 5955 . . . . . . . 8  |-  ( ( ( x  e.  X ,  y  e.  Y  |->  A ) : ( X  X.  Y ) --> Z  /\  <. x ,  y >.  e.  ( X  X.  Y ) )  ->  ( (
( z  e.  Z  |->  B )  o.  (
x  e.  X , 
y  e.  Y  |->  A ) ) `  <. x ,  y >. )  =  ( ( z  e.  Z  |->  B ) `
 ( ( x  e.  X ,  y  e.  Y  |->  A ) `
 <. x ,  y
>. ) ) )
4311, 41, 42syl2an 479 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  -> 
( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. x ,  y
>. )  =  (
( z  e.  Z  |->  B ) `  (
( x  e.  X ,  y  e.  Y  |->  A ) `  <. x ,  y >. )
) )
44 df-ov 6305 . . . . . . . 8  |-  ( x ( x  e.  X ,  y  e.  Y  |->  C ) y )  =  ( ( x  e.  X ,  y  e.  Y  |->  C ) `
 <. x ,  y
>. )
45 eqid 2422 . . . . . . . . . 10  |-  ( x  e.  X ,  y  e.  Y  |->  C )  =  ( x  e.  X ,  y  e.  Y  |->  C )
4645ovmpt4g 6430 . . . . . . . . 9  |-  ( ( x  e.  X  /\  y  e.  Y  /\  C  e.  U. M )  ->  ( x ( x  e.  X , 
y  e.  Y  |->  C ) y )  =  C )
472, 3, 37, 46syl3anc 1264 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  -> 
( x ( x  e.  X ,  y  e.  Y  |->  C ) y )  =  C )
4844, 47syl5eqr 2477 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  -> 
( ( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  y >.
)  =  C )
4940, 43, 483eqtr4d 2473 . . . . . 6  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  Y ) )  -> 
( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. x ,  y
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  y >. )
)
5049ralrimivva 2846 . . . . 5  |-  ( ph  ->  A. x  e.  X  A. y  e.  Y  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. x ,  y
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  y >. )
)
51 nfv 1751 . . . . . 6  |-  F/ u A. y  e.  Y  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. x ,  y
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  y >. )
52 nfcv 2584 . . . . . . 7  |-  F/_ x Y
53 nfcv 2584 . . . . . . . . . 10  |-  F/_ x
( z  e.  Z  |->  B )
54 nfmpt21 6369 . . . . . . . . . 10  |-  F/_ x
( x  e.  X ,  y  e.  Y  |->  A )
5553, 54nfco 5016 . . . . . . . . 9  |-  F/_ x
( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) )
56 nfcv 2584 . . . . . . . . 9  |-  F/_ x <. u ,  v >.
5755, 56nffv 5885 . . . . . . . 8  |-  F/_ x
( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. u ,  v
>. )
58 nfmpt21 6369 . . . . . . . . 9  |-  F/_ x
( x  e.  X ,  y  e.  Y  |->  C )
5958, 56nffv 5885 . . . . . . . 8  |-  F/_ x
( ( x  e.  X ,  y  e.  Y  |->  C ) `  <. u ,  v >.
)
6057, 59nfeq 2595 . . . . . . 7  |-  F/ x
( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. u ,  v
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. u ,  v >. )
6152, 60nfral 2811 . . . . . 6  |-  F/ x A. v  e.  Y  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. u ,  v
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. u ,  v >. )
62 nfv 1751 . . . . . . . 8  |-  F/ v ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. x ,  y
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  y >. )
63 nfcv 2584 . . . . . . . . . . 11  |-  F/_ y
( z  e.  Z  |->  B )
64 nfmpt22 6370 . . . . . . . . . . 11  |-  F/_ y
( x  e.  X ,  y  e.  Y  |->  A )
6563, 64nfco 5016 . . . . . . . . . 10  |-  F/_ y
( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) )
66 nfcv 2584 . . . . . . . . . 10  |-  F/_ y <. x ,  v >.
6765, 66nffv 5885 . . . . . . . . 9  |-  F/_ y
( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. x ,  v
>. )
68 nfmpt22 6370 . . . . . . . . . 10  |-  F/_ y
( x  e.  X ,  y  e.  Y  |->  C )
6968, 66nffv 5885 . . . . . . . . 9  |-  F/_ y
( ( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  v >.
)
7067, 69nfeq 2595 . . . . . . . 8  |-  F/ y ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. x ,  v
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  v >. )
71 opeq2 4185 . . . . . . . . . 10  |-  ( y  =  v  ->  <. x ,  y >.  =  <. x ,  v >. )
7271fveq2d 5882 . . . . . . . . 9  |-  ( y  =  v  ->  (
( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  <. x ,  y >.
)  =  ( ( ( z  e.  Z  |->  B )  o.  (
x  e.  X , 
y  e.  Y  |->  A ) ) `  <. x ,  v >. )
)
7371fveq2d 5882 . . . . . . . . 9  |-  ( y  =  v  ->  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  y >. )  =  ( ( x  e.  X ,  y  e.  Y  |->  C ) `
 <. x ,  v
>. ) )
7472, 73eqeq12d 2444 . . . . . . . 8  |-  ( y  =  v  ->  (
( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. x ,  y
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  y >. )  <->  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  <. x ,  v >.
)  =  ( ( x  e.  X , 
y  e.  Y  |->  C ) `  <. x ,  v >. )
) )
7562, 70, 74cbvral 3051 . . . . . . 7  |-  ( A. y  e.  Y  (
( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  <. x ,  y >.
)  =  ( ( x  e.  X , 
y  e.  Y  |->  C ) `  <. x ,  y >. )  <->  A. v  e.  Y  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  <. x ,  v >.
)  =  ( ( x  e.  X , 
y  e.  Y  |->  C ) `  <. x ,  v >. )
)
76 opeq1 4184 . . . . . . . . . 10  |-  ( x  =  u  ->  <. x ,  v >.  =  <. u ,  v >. )
7776fveq2d 5882 . . . . . . . . 9  |-  ( x  =  u  ->  (
( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  <. x ,  v >.
)  =  ( ( ( z  e.  Z  |->  B )  o.  (
x  e.  X , 
y  e.  Y  |->  A ) ) `  <. u ,  v >. )
)
7876fveq2d 5882 . . . . . . . . 9  |-  ( x  =  u  ->  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  v >. )  =  ( ( x  e.  X ,  y  e.  Y  |->  C ) `
 <. u ,  v
>. ) )
7977, 78eqeq12d 2444 . . . . . . . 8  |-  ( x  =  u  ->  (
( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. x ,  v
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  v >. )  <->  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  <. u ,  v >.
)  =  ( ( x  e.  X , 
y  e.  Y  |->  C ) `  <. u ,  v >. )
) )
8079ralbidv 2864 . . . . . . 7  |-  ( x  =  u  ->  ( A. v  e.  Y  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. x ,  v
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  v >. )  <->  A. v  e.  Y  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  <. u ,  v >.
)  =  ( ( x  e.  X , 
y  e.  Y  |->  C ) `  <. u ,  v >. )
) )
8175, 80syl5bb 260 . . . . . 6  |-  ( x  =  u  ->  ( A. y  e.  Y  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. x ,  y
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. x ,  y >. )  <->  A. v  e.  Y  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  <. u ,  v >.
)  =  ( ( x  e.  X , 
y  e.  Y  |->  C ) `  <. u ,  v >. )
) )
8251, 61, 81cbvral 3051 . . . . 5  |-  ( A. x  e.  X  A. y  e.  Y  (
( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  <. x ,  y >.
)  =  ( ( x  e.  X , 
y  e.  Y  |->  C ) `  <. x ,  y >. )  <->  A. u  e.  X  A. v  e.  Y  (
( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  <. u ,  v >.
)  =  ( ( x  e.  X , 
y  e.  Y  |->  C ) `  <. u ,  v >. )
)
8350, 82sylib 199 . . . 4  |-  ( ph  ->  A. u  e.  X  A. v  e.  Y  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. u ,  v
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. u ,  v >. )
)
84 fveq2 5878 . . . . . 6  |-  ( w  =  <. u ,  v
>.  ->  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  w )  =  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  <. u ,  v >. )
)
85 fveq2 5878 . . . . . 6  |-  ( w  =  <. u ,  v
>.  ->  ( ( x  e.  X ,  y  e.  Y  |->  C ) `
 w )  =  ( ( x  e.  X ,  y  e.  Y  |->  C ) `  <. u ,  v >.
) )
8684, 85eqeq12d 2444 . . . . 5  |-  ( w  =  <. u ,  v
>.  ->  ( ( ( ( z  e.  Z  |->  B )  o.  (
x  e.  X , 
y  e.  Y  |->  A ) ) `  w
)  =  ( ( x  e.  X , 
y  e.  Y  |->  C ) `  w )  <-> 
( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. u ,  v
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. u ,  v >. )
) )
8786ralxp 4992 . . . 4  |-  ( A. w  e.  ( X  X.  Y ) ( ( ( z  e.  Z  |->  B )  o.  (
x  e.  X , 
y  e.  Y  |->  A ) ) `  w
)  =  ( ( x  e.  X , 
y  e.  Y  |->  C ) `  w )  <->  A. u  e.  X  A. v  e.  Y  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 <. u ,  v
>. )  =  (
( x  e.  X ,  y  e.  Y  |->  C ) `  <. u ,  v >. )
)
8883, 87sylibr 215 . . 3  |-  ( ph  ->  A. w  e.  ( X  X.  Y ) ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `
 w )  =  ( ( x  e.  X ,  y  e.  Y  |->  C ) `  w ) )
89 fco 5753 . . . . . 6  |-  ( ( ( z  e.  Z  |->  B ) : Z --> U. M  /\  (
x  e.  X , 
y  e.  Y  |->  A ) : ( X  X.  Y ) --> Z )  ->  ( (
z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) : ( X  X.  Y ) --> U. M )
9029, 11, 89syl2anc 665 . . . . 5  |-  ( ph  ->  ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) : ( X  X.  Y
) --> U. M )
91 ffn 5743 . . . . 5  |-  ( ( ( z  e.  Z  |->  B )  o.  (
x  e.  X , 
y  e.  Y  |->  A ) ) : ( X  X.  Y ) --> U. M  ->  (
( z  e.  Z  |->  B )  o.  (
x  e.  X , 
y  e.  Y  |->  A ) )  Fn  ( X  X.  Y ) )
9290, 91syl 17 . . . 4  |-  ( ph  ->  ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) )  Fn  ( X  X.  Y
) )
9337ralrimivva 2846 . . . . . 6  |-  ( ph  ->  A. x  e.  X  A. y  e.  Y  C  e.  U. M )
9445fmpt2 6871 . . . . . 6  |-  ( A. x  e.  X  A. y  e.  Y  C  e.  U. M  <->  ( x  e.  X ,  y  e.  Y  |->  C ) : ( X  X.  Y
) --> U. M )
9593, 94sylib 199 . . . . 5  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  C ) : ( X  X.  Y ) --> U. M )
96 ffn 5743 . . . . 5  |-  ( ( x  e.  X , 
y  e.  Y  |->  C ) : ( X  X.  Y ) --> U. M  ->  ( x  e.  X ,  y  e.  Y  |->  C )  Fn  ( X  X.  Y
) )
9795, 96syl 17 . . . 4  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  C )  Fn  ( X  X.  Y ) )
98 eqfnfv 5988 . . . 4  |-  ( ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) )  Fn  ( X  X.  Y
)  /\  ( x  e.  X ,  y  e.  Y  |->  C )  Fn  ( X  X.  Y
) )  ->  (
( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) )  =  ( x  e.  X ,  y  e.  Y  |->  C )  <->  A. w  e.  ( X  X.  Y
) ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  w )  =  ( ( x  e.  X ,  y  e.  Y  |->  C ) `
 w ) ) )
9992, 97, 98syl2anc 665 . . 3  |-  ( ph  ->  ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) )  =  ( x  e.  X ,  y  e.  Y  |->  C )  <->  A. w  e.  ( X  X.  Y
) ( ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) ) `  w )  =  ( ( x  e.  X ,  y  e.  Y  |->  C ) `
 w ) ) )
10088, 99mpbird 235 . 2  |-  ( ph  ->  ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) )  =  ( x  e.  X ,  y  e.  Y  |->  C ) )
101 cnco 20269 . . 3  |-  ( ( ( x  e.  X ,  y  e.  Y  |->  A )  e.  ( ( J  tX  K
)  Cn  L )  /\  ( z  e.  Z  |->  B )  e.  ( L  Cn  M
) )  ->  (
( z  e.  Z  |->  B )  o.  (
x  e.  X , 
y  e.  Y  |->  A ) )  e.  ( ( J  tX  K
)  Cn  M ) )
1029, 22, 101syl2anc 665 . 2  |-  ( ph  ->  ( ( z  e.  Z  |->  B )  o.  ( x  e.  X ,  y  e.  Y  |->  A ) )  e.  ( ( J  tX  K )  Cn  M
) )
103100, 102eqeltrrd 2511 1  |-  ( ph  ->  ( x  e.  X ,  y  e.  Y  |->  C )  e.  ( ( J  tX  K
)  Cn  M ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1868   A.wral 2775   <.cop 4002   U.cuni 4216    |-> cmpt 4479    X. cxp 4848    o. ccom 4854    Fn wfn 5593   -->wf 5594   ` cfv 5598  (class class class)co 6302    |-> cmpt2 6304   Topctop 19904  TopOnctopon 19905    Cn ccn 20227    tX ctx 20562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-fv 5606  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-1st 6804  df-2nd 6805  df-map 7479  df-topgen 15330  df-top 19908  df-bases 19909  df-topon 19910  df-cn 20230  df-tx 20564
This theorem is referenced by:  cnmpt21f  20674  xkofvcn  20686  xkohmeo  20817  qustgplem  21122  prdstmdd  21125  divcn  21887  htpycom  21994  htpycc  21998  reparphti  22015  pcocn  22035  pcohtpylem  22037  pcopt  22040  pcopt2  22041  pcoass  22042  pcorevlem  22044  dipcn  26345
  Copyright terms: Public domain W3C validator