Metamath Proof Explorer

Theorem cnextfval

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

Ref Expression
Hypotheses cnextfval.1 
|- X = U. J
cnextfval.2 
|- B = U. K
Assertion cnextfval 
|- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> ( ( J CnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )

Proof

Step Hyp Ref Expression
1 cnextfval.1 
 |-  X = U. J
2 cnextfval.2 
 |-  B = U. K
3 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 ) ) ) )
4 3 adantr 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> ( 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 ) ) ) )
5 simpr 
 |-  ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> f = F )
6 5 dmeqd 
 |-  ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> dom f = dom F )
7 simplrl 
 |-  ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> F : A --> B )
8 7 fdmd 
 |-  ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> dom F = A )
9 6 8 eqtrd 
 |-  ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> dom f = A )
10 9 fveq2d 
 |-  ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> ( ( cls ` J ) ` dom f ) = ( ( cls ` J ) ` A ) )
11 9 oveq2d 
 |-  ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> ( ( ( nei ` J ) ` { x } ) |`t dom f ) = ( ( ( nei ` J ) ` { x } ) |`t A ) )
12 11 oveq2d 
 |-  ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) = ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) )
13 12 5 fveq12d 
 |-  ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) = ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
14 13 xpeq2d 
 |-  ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) = ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
15 10 14 iuneq12d 
 |-  ( ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) /\ f = F ) -> U_ x e. ( ( cls ` J ) ` dom f ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t dom f ) ) ` f ) ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
16 uniexg 
 |-  ( K e. Top -> U. K e. _V )
17 16 ad2antlr 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> U. K e. _V )
18 uniexg 
 |-  ( J e. Top -> U. J e. _V )
19 18 ad2antrr 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> U. J e. _V )
20 eqid 
 |-  A = A
21 20 2 feq23i 
 |-  ( F : A --> B <-> F : A --> U. K )
22 21 biimpi 
 |-  ( F : A --> B -> F : A --> U. K )
23 22 ad2antrl 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> F : A --> U. K )
24 1 sseq2i 
 |-  ( A C_ X <-> A C_ U. J )
25 24 biimpi 
 |-  ( A C_ X -> A C_ U. J )
26 25 ad2antll 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> A C_ U. J )
27 elpm2r 
 |-  ( ( ( U. K e. _V /\ U. J e. _V ) /\ ( F : A --> U. K /\ A C_ U. J ) ) -> F e. ( U. K ^pm U. J ) )
28 17 19 23 26 27 syl22anc 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> F e. ( U. K ^pm U. J ) )
29 fvex 
 |-  ( ( cls ` J ) ` A ) e. _V
30 vsnex 
 |-  { x } e. _V
31 fvex 
 |-  ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) e. _V
32 30 31 xpex 
 |-  ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) e. _V
33 29 32 iunex 
 |-  U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) e. _V
34 33 a1i 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) e. _V )
35 4 15 28 34 fvmptd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ X ) ) -> ( ( J CnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )