Metamath Proof Explorer

Theorem cnextval

Description: The function applying continuous extension to a given function f . (Contributed by Thierry Arnoux, 1-Dec-2017)

Ref Expression
Assertion cnextval 
|- ( ( J e. Top /\ K e. Top ) -> ( J CnExt K ) = ( f e. ( U. K ^pm U. J ) |-> U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) ) )

Proof

Step Hyp Ref Expression
1 unieq 
 |-  ( j = J -> U. j = U. J )
2 1 oveq2d 
 |-  ( j = J -> ( U. k ^pm U. j ) = ( U. k ^pm U. J ) )
3 fveq2 
 |-  ( j = J -> ( cls ` j ) = ( cls ` J ) )
4 3 fveq1d 
 |-  ( j = J -> ( ( cls ` j ) ` dom f ) = ( ( cls ` J ) ` dom f ) )
5 fveq2 
 |-  ( j = J -> ( nei ` j ) = ( nei ` J ) )
6 5 fveq1d 
 |-  ( j = J -> ( ( nei ` j ) ` { x } ) = ( ( nei ` J ) ` { x } ) )
7 6 oveq1d 
 |-  ( j = J -> ( ( ( nei ` j ) ` { x } ) |`t dom f ) = ( ( ( nei ` J ) ` { x } ) |`t dom f ) )
8 7 oveq2d 
 |-  ( j = J -> ( k fLimf ( ( ( nei ` j ) ` { x } ) |`t dom f ) ) = ( k fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) )
9 8 fveq1d 
 |-  ( j = J -> ( ( k fLimf ( ( ( nei ` j ) ` { x } ) |`t dom f ) ) ` f ) = ( ( k fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) )
10 9 xpeq2d 
 |-  ( j = J -> ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) |`t dom f ) ) ` f ) ) = ( { x } X. ( ( k fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) )
11 4 10 iuneq12d 
 |-  ( j = J -> U_ x e. ( ( cls ` j ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) |`t dom f ) ) ` f ) ) = U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) )
12 2 11 mpteq12dv 
 |-  ( j = J -> ( f e. ( U. k ^pm U. j ) |-> U_ x e. ( ( cls ` j ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) |`t dom f ) ) ` f ) ) ) = ( f e. ( U. k ^pm U. J ) |-> U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) ) )
13 unieq 
 |-  ( k = K -> U. k = U. K )
14 13 oveq1d 
 |-  ( k = K -> ( U. k ^pm U. J ) = ( U. K ^pm U. J ) )
15 oveq1 
 |-  ( k = K -> ( k fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) = ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) )
16 15 fveq1d 
 |-  ( k = K -> ( ( k fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) = ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) )
17 16 xpeq2d 
 |-  ( k = K -> ( { x } X. ( ( k fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) = ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) )
18 17 iuneq2d 
 |-  ( k = K -> U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) = U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) )
19 14 18 mpteq12dv 
 |-  ( k = K -> ( f e. ( U. k ^pm U. J ) |-> U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) ) = ( f e. ( U. K ^pm U. J ) |-> U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) ) )
20 df-cnext 
 |-  CnExt = ( j e. Top , k e. Top |-> ( f e. ( U. k ^pm U. j ) |-> U_ x e. ( ( cls ` j ) ` dom f ) ( { x } X. ( ( k fLimf ( ( ( nei ` j ) ` { x } ) |`t dom f ) ) ` f ) ) ) )
21 ovex 
 |-  ( U. K ^pm U. J ) e. _V
22 21 mptex 
 |-  ( f e. ( U. K ^pm U. J ) |-> U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) ) e. _V
23 12 19 20 22 ovmpo 
 |-  ( ( J e. Top /\ K e. Top ) -> ( J CnExt K ) = ( f e. ( U. K ^pm U. J ) |-> U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) ) )