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