This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnextfun

Description: If the target space is Hausdorff, a continuous extension is a function. (Contributed by Thierry Arnoux, 20-Dec-2017)

Ref Expression
Hypotheses cnextfrel.1 
|- C = U. J
cnextfrel.2 
|- B = U. K
Assertion cnextfun 
|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Fun ( ( J CnExt K ) ` F ) )

Proof

Step Hyp Ref Expression
1 cnextfrel.1 
 |-  C = U. J
2 cnextfrel.2 
 |-  B = U. K
3 haustop 
 |-  ( K e. Haus -> K e. Top )
4 1 2 cnextrel 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> Rel ( ( J CnExt K ) ` F ) )
5 3 4 sylanl2 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Rel ( ( J CnExt K ) ` F ) )
6 simpllr 
 |-  ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> K e. Haus )
7 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` C ) )
8 7 biimpi 
 |-  ( J e. Top -> J e. ( TopOn ` C ) )
9 8 ad3antrrr 
 |-  ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> J e. ( TopOn ` C ) )
10 simplrr 
 |-  ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> A C_ C )
11 9 7 sylibr 
 |-  ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> J e. Top )
12 1 clsss3 
 |-  ( ( J e. Top /\ A C_ C ) -> ( ( cls ` J ) ` A ) C_ C )
13 11 10 12 syl2anc 
 |-  ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> ( ( cls ` J ) ` A ) C_ C )
14 simpr 
 |-  ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> x e. ( ( cls ` J ) ` A ) )
15 13 14 sseldd 
 |-  ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> x e. C )
16 trnei 
 |-  ( ( J e. ( TopOn ` C ) /\ A C_ C /\ x e. C ) -> ( x e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) ) )
17 16 biimpa 
 |-  ( ( ( J e. ( TopOn ` C ) /\ A C_ C /\ x e. C ) /\ x e. ( ( cls ` J ) ` A ) ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) )
18 9 10 15 14 17 syl31anc 
 |-  ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) )
19 simplrl 
 |-  ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> F : A --> B )
20 2 hausflf 
 |-  ( ( K e. Haus /\ ( ( ( nei ` J ) ` { x } ) |`t A ) e. ( Fil ` A ) /\ F : A --> B ) -> E* y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
21 6 18 19 20 syl3anc 
 |-  ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> E* y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) )
22 21 ex 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( x e. ( ( cls ` J ) ` A ) -> E* y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
23 22 alrimiv 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> A. x ( x e. ( ( cls ` J ) ` A ) -> E* y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
24 moanimv 
 |-  ( 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 ) ) )
25 24 albii 
 |-  ( A. x E* y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) <-> A. x ( x e. ( ( cls ` J ) ` A ) -> E* y y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
26 23 25 sylibr 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> A. x E* y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) )
27 df-br 
 |-  ( x ( ( J CnExt K ) ` F ) y <-> <. x , y >. e. ( ( J CnExt K ) ` F ) )
28 27 a1i 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( x ( ( J CnExt K ) ` F ) y <-> <. x , y >. e. ( ( J CnExt K ) ` F ) ) )
29 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 ) ) )
30 3 29 sylanl2 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( 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 ) ) )
31 30 eleq2d 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( <. 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 ) ) ) )
32 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 ) ) )
33 32 a1i 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( <. 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 ) ) ) )
34 28 31 33 3bitrd 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( x ( ( J CnExt K ) ` F ) y <-> ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) )
35 34 mobidv 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( E* y x ( ( J CnExt K ) ` F ) y <-> E* y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) )
36 35 albidv 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( A. x E* y x ( ( J CnExt K ) ` F ) y <-> A. x E* y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) |`t A ) ) ` F ) ) ) )
37 26 36 mpbird 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> A. x E* y x ( ( J CnExt K ) ` F ) y )
38 dffun6 
 |-  ( Fun ( ( J CnExt K ) ` F ) <-> ( Rel ( ( J CnExt K ) ` F ) /\ A. x E* y x ( ( J CnExt K ) ` F ) y ) )
39 5 37 38 sylanbrc 
 |-  ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Fun ( ( J CnExt K ) ` F ) )