Metamath Proof Explorer


Theorem cnextf

Description: Extension by continuity. The extension by continuity is a function. (Contributed by Thierry Arnoux, 25-Dec-2017)

Ref Expression
Hypotheses cnextf.1
|- C = U. J
cnextf.2
|- B = U. K
cnextf.3
|- ( ph -> J e. Top )
cnextf.4
|- ( ph -> K e. Haus )
cnextf.5
|- ( ph -> F : A --> B )
cnextf.a
|- ( ph -> A C_ C )
cnextf.6
|- ( ph -> ( ( cls ` J ) ` A ) = C )
cnextf.7
|- ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) )
Assertion cnextf
|- ( ph -> ( ( J CnExt K ) ` F ) : C --> B )

Proof

Step Hyp Ref Expression
1 cnextf.1
 |-  C = U. J
2 cnextf.2
 |-  B = U. K
3 cnextf.3
 |-  ( ph -> J e. Top )
4 cnextf.4
 |-  ( ph -> K e. Haus )
5 cnextf.5
 |-  ( ph -> F : A --> B )
6 cnextf.a
 |-  ( ph -> A C_ C )
7 cnextf.6
 |-  ( ph -> ( ( cls ` J ) ` A ) = C )
8 cnextf.7
 |-  ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) )
9 1 2 cnextfun
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Fun ( ( J CnExt K ) ` F ) )
10 3 4 5 6 9 syl22anc
 |-  ( ph -> Fun ( ( J CnExt K ) ` F ) )
11 dfdm3
 |-  dom ( ( J CnExt K ) ` F ) = { x | E. y <. x , y >. e. ( ( J CnExt K ) ` F ) }
12 simpl
 |-  ( ( ph /\ x e. C ) -> ph )
13 7 eleq2d
 |-  ( ph -> ( x e. ( ( cls ` J ) ` A ) <-> x e. C ) )
14 13 biimpar
 |-  ( ( ph /\ x e. C ) -> x e. ( ( cls ` J ) ` A ) )
15 n0
 |-  ( ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) =/= (/) <-> E. y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
16 8 15 sylib
 |-  ( ( ph /\ x e. C ) -> E. y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
17 haustop
 |-  ( K e. Haus -> K e. Top )
18 4 17 syl
 |-  ( ph -> K e. Top )
19 1 2 cnextfval
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> ( ( J CnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
20 3 18 5 6 19 syl22anc
 |-  ( ph -> ( ( J CnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
21 20 eleq2d
 |-  ( ph -> ( <. x , y >. e. ( ( J CnExt K ) ` F ) <-> <. x , y >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) )
22 opeliunxp
 |-  ( <. x , y >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
23 21 22 bitrdi
 |-  ( ph -> ( <. x , y >. e. ( ( J CnExt K ) ` F ) <-> ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) )
24 23 exbidv
 |-  ( ph -> ( E. y <. x , y >. e. ( ( J CnExt K ) ` F ) <-> E. y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) )
25 19.42v
 |-  ( E. y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> ( x e. ( ( cls ` J ) ` A ) /\ E. y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
26 24 25 bitrdi
 |-  ( ph -> ( E. y <. x , y >. e. ( ( J CnExt K ) ` F ) <-> ( x e. ( ( cls ` J ) ` A ) /\ E. y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) )
27 26 biimpar
 |-  ( ( ph /\ ( x e. ( ( cls ` J ) ` A ) /\ E. y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) -> E. y <. x , y >. e. ( ( J CnExt K ) ` F ) )
28 12 14 16 27 syl12anc
 |-  ( ( ph /\ x e. C ) -> E. y <. x , y >. e. ( ( J CnExt K ) ` F ) )
29 26 simprbda
 |-  ( ( ph /\ E. y <. x , y >. e. ( ( J CnExt K ) ` F ) ) -> x e. ( ( cls ` J ) ` A ) )
30 13 adantr
 |-  ( ( ph /\ E. y <. x , y >. e. ( ( J CnExt K ) ` F ) ) -> ( x e. ( ( cls ` J ) ` A ) <-> x e. C ) )
31 29 30 mpbid
 |-  ( ( ph /\ E. y <. x , y >. e. ( ( J CnExt K ) ` F ) ) -> x e. C )
32 28 31 impbida
 |-  ( ph -> ( x e. C <-> E. y <. x , y >. e. ( ( J CnExt K ) ` F ) ) )
33 32 abbi2dv
 |-  ( ph -> C = { x | E. y <. x , y >. e. ( ( J CnExt K ) ` F ) } )
34 11 33 eqtr4id
 |-  ( ph -> dom ( ( J CnExt K ) ` F ) = C )
35 df-fn
 |-  ( ( ( J CnExt K ) ` F ) Fn C <-> ( Fun ( ( J CnExt K ) ` F ) /\ dom ( ( J CnExt K ) ` F ) = C ) )
36 10 34 35 sylanbrc
 |-  ( ph -> ( ( J CnExt K ) ` F ) Fn C )
37 20 rneqd
 |-  ( ph -> ran ( ( J CnExt K ) ` F ) = ran U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
38 rniun
 |-  ran U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) = U_ x e. ( ( cls ` J ) ` A ) ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
39 vex
 |-  x e. _V
40 39 snnz
 |-  { x } =/= (/)
41 rnxp
 |-  ( { x } =/= (/) -> ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) = ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
42 40 41 ax-mp
 |-  ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) = ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F )
43 13 biimpa
 |-  ( ( ph /\ x e. ( ( cls ` J ) ` A ) ) -> x e. C )
44 2 toptopon
 |-  ( K e. Top <-> K e. ( TopOn ` B ) )
45 18 44 sylib
 |-  ( ph -> K e. ( TopOn ` B ) )
46 45 adantr
 |-  ( ( ph /\ x e. C ) -> K e. ( TopOn ` B ) )
47 1 toptopon
 |-  ( J e. Top <-> J e. ( TopOn ` C ) )
48 3 47 sylib
 |-  ( ph -> J e. ( TopOn ` C ) )
49 48 adantr
 |-  ( ( ph /\ x e. C ) -> J e. ( TopOn ` C ) )
50 6 adantr
 |-  ( ( ph /\ x e. C ) -> A C_ C )
51 simpr
 |-  ( ( ph /\ x e. C ) -> x e. C )
52 trnei
 |-  ( ( J e. ( TopOn ` C ) /\ A C_ C /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) )
53 52 biimpa
 |-  ( ( ( J e. ( TopOn ` C ) /\ A C_ C /\ x e. C ) /\ x e. ( ( cls ` J ) ` A ) ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) )
54 49 50 51 14 53 syl31anc
 |-  ( ( ph /\ x e. C ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) )
55 5 adantr
 |-  ( ( ph /\ x e. C ) -> F : A --> B )
56 flfelbas
 |-  ( ( ( K e. ( TopOn ` B ) /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) -> y e. B )
57 56 ex
 |-  ( ( K e. ( TopOn ` B ) /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) -> ( y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) -> y e. B ) )
58 57 ssrdv
 |-  ( ( K e. ( TopOn ` B ) /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) C_ B )
59 46 54 55 58 syl3anc
 |-  ( ( ph /\ x e. C ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) C_ B )
60 43 59 syldan
 |-  ( ( ph /\ x e. ( ( cls ` J ) ` A ) ) -> ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) C_ B )
61 42 60 eqsstrid
 |-  ( ( ph /\ x e. ( ( cls ` J ) ` A ) ) -> ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) C_ B )
62 61 ralrimiva
 |-  ( ph -> A. x e. ( ( cls ` J ) ` A ) ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) C_ B )
63 iunss
 |-  ( U_ x e. ( ( cls ` J ) ` A ) ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) C_ B <-> A. x e. ( ( cls ` J ) ` A ) ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) C_ B )
64 62 63 sylibr
 |-  ( ph -> U_ x e. ( ( cls ` J ) ` A ) ran ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) C_ B )
65 38 64 eqsstrid
 |-  ( ph -> ran U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) C_ B )
66 37 65 eqsstrd
 |-  ( ph -> ran ( ( J CnExt K ) ` F ) C_ B )
67 df-f
 |-  ( ( ( J CnExt K ) ` F ) : C --> B <-> ( ( ( J CnExt K ) ` F ) Fn C /\ ran ( ( J CnExt K ) ` F ) C_ B ) )
68 36 66 67 sylanbrc
 |-  ( ph -> ( ( J CnExt K ) ` F ) : C --> B )