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 )