Theorem cnextfun 21157

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

Hypotheses

Ref	Expression
cnextfrel.1	|- C = U. J
cnextfrel.2	|- B = U. K

Assertion

Ref	Expression
cnextfun	|- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Fun ( ( JCnExt K ) ` F ) )

Proof of Theorem cnextfun

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		haustop 20424	. . 3 |- ( K e. Haus -> K e. Top )
2		cnextfrel.1	. . . 4 |- C = U. J
3		cnextfrel.2	. . . 4 |- B = U. K
4	2, 3	cnextrel 21156	. . 3 |- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> Rel ( ( JCnExt K ) ` F ) )
5	1, 4	sylanl2 663	. 2 |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Rel ( ( JCnExt K ) ` F ) )
6		simpllr 777	. . . . . . 7 |- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> K e. Haus )
7	2	toptopon 20025	. . . . . . . . . 10 |- ( J e. Top <-> J e. (TopOn ` C ) )
8	7	biimpi 199	. . . . . . . . 9 |- ( J e. Top -> J e. (TopOn ` C ) )
9	8	ad3antrrr 744	. . . . . . . 8 |- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> J e. (TopOn ` C ) )
10		simplrr 779	. . . . . . . 8 |- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> A C_ C )
11	9, 7	sylibr 217	. . . . . . . . . 10 |- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> J e. Top )
12	2	clsss3 20151	. . . . . . . . . 10 |- ( ( J e. Top /\ A C_ C ) -> ( ( cls ` J ) ` A ) C_ C )
13	11, 10, 12	syl2anc 673	. . . . . . . . 9 |- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> ( ( cls ` J ) ` A ) C_ C )
14		simpr 468	. . . . . . . . 9 |- ( ( ( ( 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 3419	. . . . . . . 8 |- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> x e. C )
16		trnei 20985	. . . . . . . . 9 |- ( ( 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 492	. . . . . . . 8 |- ( ( ( 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 1295	. . . . . . 7 |- ( ( ( ( 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 778	. . . . . . 7 |- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> F : A --> B )
20	3	hausflf 21090	. . . . . . 7 |- ( ( 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 1292	. . . . . 6 |- ( ( ( ( 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 441	. . . . 5 |- ( ( ( 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 1781	. . . 4 |- ( ( ( 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 2380	. . . . 5 |- ( 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 1699	. . . 4 |- ( 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 217	. . 3 |- ( ( ( 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 4396	. . . . . . 7 |- ( x ( ( JCnExt K ) ` F ) y <-> <. x , y >. e. ( ( JCnExt K ) ` F ) )
28	27	a1i 11	. . . . . 6 |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( x ( ( JCnExt K ) ` F ) y <-> <. x , y >. e. ( ( JCnExt K ) ` F ) ) )
29	2, 3	cnextfval 21155	. . . . . . . 8 |- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> ( ( JCnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) ) )
30	1, 29	sylanl2 663	. . . . . . 7 |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( ( JCnExt K ) ` F ) = U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) ) )
31	30	eleq2d 2534	. . . . . 6 |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( <. x , y >. e. ( ( JCnExt K ) ` F ) <-> <. x , y >. e. U_ x e. ( ( cls ` J ) ` A ) ( { x } X. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) ) ) )
32		opeliunxp 4891	. . . . . . 7 |- ( <. 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 11	. . . . . 6 |- ( ( ( 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 287	. . . . 5 |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( x ( ( JCnExt K ) ` F ) y <-> ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) ) ) )
35	34	mobidv 2340	. . . 4 |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( E* y x ( ( JCnExt K ) ` F ) y <-> E* y ( x e. ( ( cls ` J ) ` A ) /\ y e. ( ( K fLimf ( ( ( nei ` J ) ` { x } ) ↾t A ) ) ` F ) ) ) )
36	35	albidv 1775	. . 3 |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> ( A. x E* y x ( ( JCnExt 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 240	. 2 |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> A. x E* y x ( ( JCnExt K ) ` F ) y )
38		dffun6 5604	. 2 |- ( Fun ( ( JCnExt K ) ` F ) <-> ( Rel ( ( JCnExt K ) ` F ) /\ A. x E* y x ( ( JCnExt K ) ` F ) y ) )
39	5, 37, 38	sylanbrc 677	1 |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Fun ( ( JCnExt K ) ` F ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   /\ w3a 1007   A.wal 1450   = wceq 1452   e. wcel 1904   E*wmo 2320   C_ wss 3390   {csn 3959   <.cop 3965   U.cuni 4190   U_ciun 4269   class class class wbr 4395   X. cxp 4837   Rel wrel 4844   Fun wfun 5583   -->wf 5585   ` cfv 5589  (class class class)co 6308   ↾_t crest 15397   Topctop 19994  TopOnctopon 19995   clsccl 20110   neicnei 20190   Hauscha 20401   Filcfil 20938   fLimf cflf 21028  CnExtccnext 21152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-1st 6812  df-2nd 6813  df-map 7492  df-pm 7493  df-rest 15399  df-fbas 19044  df-top 19998  df-topon 20000  df-cld 20111  df-ntr 20112  df-cls 20113  df-nei 20191  df-haus 20408  df-fil 20939  df-flim 21032  df-flf 21033  df-cnext 21153

This theorem is referenced by:  cnextfvval  21158  cnextf  21159  cnextfres  21162