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 snex
 |-  { 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 ) ) )