Theorem cnextfun 19763

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 19062	. . 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 19762	. . 3 |- ( ( ( J e. Top /\ K e. Top ) /\ ( F : A --> B /\ A C_ C ) ) -> Rel ( ( JCnExt K ) ` F ) )
5	1, 4	sylanl2 651	. 2 |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Rel ( ( JCnExt K ) ` F ) )
6		simpllr 758	. . . . . . 7 |- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> K e. Haus )
7	2	toptopon 18665	. . . . . . . . . 10 |- ( J e. Top <-> J e. (TopOn ` C ) )
8	7	biimpi 194	. . . . . . . . 9 |- ( J e. Top -> J e. (TopOn ` C ) )
9	8	ad3antrrr 729	. . . . . . . 8 |- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> J e. (TopOn ` C ) )
10		simplrr 760	. . . . . . . 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 212	. . . . . . . . . 10 |- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> J e. Top )
12	2	clsss3 18790	. . . . . . . . . 10 |- ( ( J e. Top /\ A C_ C ) -> ( ( cls ` J ) ` A ) C_ C )
13	11, 10, 12	syl2anc 661	. . . . . . . . 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 461	. . . . . . . . 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 3460	. . . . . . . 8 |- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> x e. C )
16		trnei 19592	. . . . . . . . 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 484	. . . . . . . 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 1222	. . . . . . 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 759	. . . . . . 7 |- ( ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) /\ x e. ( ( cls ` J ) ` A ) ) -> F : A --> B )
20	3	hausflf 19697	. . . . . . 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 1219	. . . . . 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 434	. . . . 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 1686	. . . 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 2342	. . . . 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 1611	. . . 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 212	. . 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 19761	. . . . . . . 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 651	. . . . . . 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 2522	. . . . . 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 4993	. . . . . . 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 279	. . . . 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 2285	. . . 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 1680	. . 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 232	. 2 |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> A. x E* y x ( ( JCnExt K ) ` F ) y )
38		dffun6 5536	. 2 |- ( Fun ( ( JCnExt K ) ` F ) <-> ( Rel ( ( JCnExt K ) ` F ) /\ A. x E* y x ( ( JCnExt K ) ` F ) y ) )
39	5, 37, 38	sylanbrc 664	1 |- ( ( ( J e. Top /\ K e. Haus ) /\ ( F : A --> B /\ A C_ C ) ) -> Fun ( ( JCnExt K ) ` F ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   A.wal 1368   = wceq 1370   e. wcel 1758   E*wmo 2262   C_ wss 3431   {csn 3980   <.cop 3986   U.cuni 4194   U_ciun 4274   class class class wbr 4395   X. cxp 4941   Rel wrel 4948   Fun wfun 5515   -->wf 5517   ` cfv 5521  (class class class)co 6195   ↾_t crest 14473   Topctop 18625  TopOnctopon 18626   clsccl 18749   neicnei 18828   Hauscha 19039   Filcfil 19545   fLimf cflf 19635  CnExtccnext 19758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4573  ax-pr 4634  ax-un 6477

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2265  df-mo 2266  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-nel 2648  df-ral 2801  df-rex 2802  df-reu 2803  df-rab 2805  df-v 3074  df-sbc 3289  df-csb 3391  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4195  df-int 4232  df-iun 4276  df-iin 4277  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4739  df-xp 4949  df-rel 4950  df-cnv 4951  df-co 4952  df-dm 4953  df-rn 4954  df-res 4955  df-ima 4956  df-iota 5484  df-fun 5523  df-fn 5524  df-f 5525  df-f1 5526  df-fo 5527  df-f1o 5528  df-fv 5529  df-ov 6198  df-oprab 6199  df-mpt2 6200  df-1st 6682  df-2nd 6683  df-map 7321  df-pm 7322  df-rest 14475  df-fbas 17934  df-top 18630  df-topon 18633  df-cld 18750  df-ntr 18751  df-cls 18752  df-nei 18829  df-haus 19046  df-fil 19546  df-flim 19639  df-flf 19640  df-cnext 19759

This theorem is referenced by:  cnextfvval  19764  cnextf  19765