Theorem cnpfillim4 14947

Description: If G is continuous at point A, and the filter base F converges to A then G(F) converges to G(A).

Hypotheses

Ref	Expression
cnfillim4.1	|- X = U.J
cnfillim4.2	|- Y = U.K

Assertion

Ref	Expression
cnpfillim4	|- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> (G` A) e. ((fLim1` K)` ((Y FilMap F)` G)))

Proof of Theorem cnpfillim4

Step	Hyp	Ref	Expression
1		simpl2 880	. . 3 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> K e. Top)
2		uniexg 3795	. . . . . . 7 |- (K e. Top -> U.K e. _V)
3		cnfillim4.2	. . . . . . 7 |- Y = U.K
4	2, 3	syl5eqel 1975	. . . . . 6 |- (K e. Top -> Y e. _V)
5	4	3ad2ant2 898	. . . . 5 |- ((J e. Top /\ K e. Top /\ F e. fBas) -> Y e. _V)
6	5	adantr 425	. . . 4 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> Y e. _V)
7		simpl1 879	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> J e. Top)
8		fgfil 10290	. . . . . . . . . 10 |- (F e. fBas -> (filGen` F) e. Fil)
9	8	3ad2ant3 899	. . . . . . . . 9 |- ((J e. Top /\ K e. Top /\ F e. fBas) -> (filGen` F) e. Fil)
10	9	adantr 425	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> (filGen` F) e. Fil)
11		eqeq1 1890	. . . . . . . . . . . . 13 |- (X = U.F -> (X = U.(filGen` F) <-> U.F = U.(filGen` F)))
12		eqid 1884	. . . . . . . . . . . . . 14 |- U.F = U.F
13	12	fgbas 10286	. . . . . . . . . . . . 13 |- (F e. fBas -> U.F = U.(filGen` F))
14	11, 13	syl5bir 227	. . . . . . . . . . . 12 |- (X = U.F -> (F e. fBas -> X = U.(filGen` F)))
15	14	3ad2ant3 899	. . . . . . . . . . 11 |- ((G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F) -> (F e. fBas -> X = U.(filGen` F)))
16	15	com12 14	. . . . . . . . . 10 |- (F e. fBas -> ((G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F) -> X = U.(filGen` F)))
17	16	3ad2ant3 899	. . . . . . . . 9 |- ((J e. Top /\ K e. Top /\ F e. fBas) -> ((G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F) -> X = U.(filGen` F)))
18	17	imp 377	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> X = U.(filGen` F))
19		simpr2 883	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> A e. ((fLim1` J)` (filGen` F)))
20		cnfillim4.1	. . . . . . . . 9 |- X = U.J
21		eqid 1884	. . . . . . . . 9 |- U.(filGen` F) = U.(filGen` F)
22	20, 21	flimelbas 10300	. . . . . . . 8 |- (((J e. Top /\ (filGen` F) e. Fil /\ X = U.(filGen` F)) /\ A e. ((fLim1` J)` (filGen` F))) -> A e. X)
23	7, 10, 18, 19, 22	syl31anc 1103	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> A e. X)
24		simpl 346	. . . . . . . 8 |- ((J e. Top /\ A e. X) -> J e. Top)
25		snssi 3129	. . . . . . . . 9 |- (A e. X -> {A} C_ X)
26	25	adantl 424	. . . . . . . 8 |- ((J e. Top /\ A e. X) -> {A} C_ X)
27		snnzg 3118	. . . . . . . . 9 |- (A e. X -> {A} =/= (/))
28	27	adantl 424	. . . . . . . 8 |- ((J e. Top /\ A e. X) -> {A} =/= (/))
29	24, 26, 28	3jca 1050	. . . . . . 7 |- ((J e. Top /\ A e. X) -> (J e. Top /\ {A} C_ X /\ {A} =/= (/)))
30	7, 23, 29	syl11anc 524	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> (J e. Top /\ {A} C_ X /\ {A} =/= (/)))
31	20	neifil 10302	. . . . . 6 |- ((J e. Top /\ {A} C_ X /\ {A} =/= (/)) -> ((nei` J)` {A}) e. Fil)
32	30, 31	syl 12	. . . . 5 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> ((nei` J)` {A}) e. Fil)
33		filfbas 10276	. . . . 5 |- (((nei` J)` {A}) e. Fil -> ((nei` J)` {A}) e. fBas)
34	32, 33	syl 12	. . . 4 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> ((nei` J)` {A}) e. fBas)
35		simpr1 882	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> G e. ((J CnP K)` A))
36	20, 3	cnpf 9039	. . . . . 6 |- (((J e. Top /\ K e. Top /\ A e. X) /\ G e. ((J CnP K)` A)) -> G:X-->Y)
37	7, 1, 23, 35, 36	syl31anc 1103	. . . . 5 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> G:X-->Y)
38	23	snssd 3130	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> {A} C_ X)
39	20	unnei 9011	. . . . . . 7 |- ((J e. Top /\ {A} C_ X) -> U.((nei` J)` {A}) = X)
40	7, 38, 39	syl11anc 524	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> U.((nei` J)` {A}) = X)
41	40	feq2d 4557	. . . . 5 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> (G:U.((nei` J)` {A})-->Y <-> G:X-->Y))
42	37, 41	mpbird 213	. . . 4 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> G:U.((nei` J)` {A})-->Y)
43		eqid 1884	. . . . 5 |- U.((nei` J)` {A}) = U.((nei` J)` {A})
44	43	fmf 10310	. . . 4 |- ((Y e. _V /\ ((nei` J)` {A}) e. fBas /\ G:U.((nei` J)` {A})-->Y) -> ((Y FilMap ((nei` J)` {A}))` G) e. Fil)
45	6, 34, 42, 44	syl111anc 1100	. . 3 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> ((Y FilMap ((nei` J)` {A}))` G) e. Fil)
46		simpl3 881	. . . 4 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> F e. fBas)
47		simpr3 884	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> X = U.F)
48	47	eqcomd 1889	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> U.F = X)
49	48	feq2d 4557	. . . . 5 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> (G:U.F-->Y <-> G:X-->Y))
50	37, 49	mpbird 213	. . . 4 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> G:U.F-->Y)
51	12	fmf 10310	. . . 4 |- ((Y e. _V /\ F e. fBas /\ G:U.F-->Y) -> ((Y FilMap F)` G) e. Fil)
52	6, 46, 50, 51	syl111anc 1100	. . 3 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> ((Y FilMap F)` G) e. Fil)
53	1, 45, 52	3jca 1050	. 2 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> (K e. Top /\ ((Y FilMap ((nei` J)` {A}))` G) e. Fil /\ ((Y FilMap F)` G) e. Fil))
54	43	fmbas 10311	. . . 4 |- ((Y e. _V /\ ((nei` J)` {A}) e. fBas /\ G:U.((nei` J)` {A})-->Y) -> U.((Y FilMap ((nei` J)` {A}))` G) = Y)
55	6, 34, 42, 54	syl111anc 1100	. . 3 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> U.((Y FilMap ((nei` J)` {A}))` G) = Y)
56	55	eqcomd 1889	. 2 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> Y = U.((Y FilMap ((nei` J)` {A}))` G))
57	12	fmbas 10311	. . . 4 |- ((Y e. _V /\ F e. fBas /\ G:U.F-->Y) -> U.((Y FilMap F)` G) = Y)
58	6, 46, 50, 57	syl111anc 1100	. . 3 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> U.((Y FilMap F)` G) = Y)
59	58	eqcomd 1889	. 2 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> Y = U.((Y FilMap F)` G))
60		filfbas 10276	. . . . . . 7 |- ((filGen` F) e. Fil -> (filGen` F) e. fBas)
61	8, 60	syl 12	. . . . . 6 |- (F e. fBas -> (filGen` F) e. fBas)
62	61	3ad2ant3 899	. . . . 5 |- ((J e. Top /\ K e. Top /\ F e. fBas) -> (filGen` F) e. fBas)
63	62	adantr 425	. . . 4 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> (filGen` F) e. fBas)
64	40, 18	eqtrd 1925	. . . 4 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> U.((nei` J)` {A}) = U.(filGen` F))
65	20, 21	isfillim 10298	. . . . . . 7 |- ((J e. Top /\ (filGen` F) e. Fil /\ X = U.(filGen` F)) -> (A e. ((fLim1` J)` (filGen` F)) <-> (A e. X /\ ((nei` J)` {A}) C_ (filGen` F))))
66	7, 10, 18, 65	syl111anc 1100	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> (A e. ((fLim1` J)` (filGen` F)) <-> (A e. X /\ ((nei` J)` {A}) C_ (filGen` F))))
67	19, 66	mpbid 212	. . . . 5 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> (A e. X /\ ((nei` J)` {A}) C_ (filGen` F)))
68	67	simprd 352	. . . 4 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> ((nei` J)` {A}) C_ (filGen` F))
69	43, 21	filmapss 10309	. . . 4 |- (((Y e. _V /\ ((nei` J)` {A}) e. fBas /\ (filGen` F) e. fBas) /\ (G:U.((nei` J)` {A})-->Y /\ U.((nei` J)` {A}) = U.(filGen` F) /\ ((nei` J)` {A}) C_ (filGen` F))) -> ((Y FilMap ((nei` J)` {A}))` G) C_ ((Y FilMap (filGen` F))` G))
70	6, 34, 63, 42, 64, 68, 69	syl33anc 1115	. . 3 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> ((Y FilMap ((nei` J)` {A}))` G) C_ ((Y FilMap (filGen` F))` G))
71		eqid 1884	. . . . 5 |- (filGen` F) = (filGen` F)
72	12, 71	fbfgfmeq 10315	. . . 4 |- ((Y e. _V /\ F e. fBas /\ G:U.F-->Y) -> ((Y FilMap F)` G) = ((Y FilMap (filGen` F))` G))
73	6, 46, 50, 72	syl111anc 1100	. . 3 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> ((Y FilMap F)` G) = ((Y FilMap (filGen` F))` G))
74	70, 73	sseqtr4d 2654	. 2 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> ((Y FilMap ((nei` J)` {A}))` G) C_ ((Y FilMap F)` G))
75		eqid 1884	. . . . 5 |- ((nei` J)` {A}) = ((nei` J)` {A})
76	75, 3, 20	conttnf2 14945	. . . 4 |- ((J e. Top /\ K e. Top /\ (A e. X /\ G:X-->Y)) -> (G e. ((J CnP K)` A) <-> (G` A) e. ((fLim1` K)` ((Y FilMap ((nei` J)` {A}))` G))))
77	7, 1, 23, 37, 76	syl112anc 1104	. . 3 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> (G e. ((J CnP K)` A) <-> (G` A) e. ((fLim1` K)` ((Y FilMap ((nei` J)` {A}))` G))))
78	35, 77	mpbid 212	. 2 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> (G` A) e. ((fLim1` K)` ((Y FilMap ((nei` J)` {A}))` G)))
79		eqid 1884	. . 3 |- U.((Y FilMap ((nei` J)` {A}))` G) = U.((Y FilMap ((nei` J)` {A}))` G)
80		eqid 1884	. . 3 |- U.((Y FilMap F)` G) = U.((Y FilMap F)` G)
81	3, 79, 80	limfilss 10299	. 2 |- ((((K e. Top /\ ((Y FilMap ((nei` J)` {A}))` G) e. Fil /\ ((Y FilMap F)` G) e. Fil) /\ Y = U.((Y FilMap ((nei` J)` {A}))` G) /\ Y = U.((Y FilMap F)` G)) /\ ((Y FilMap ((nei` J)` {A}))` G) C_ ((Y FilMap F)` G) /\ (G` A) e. ((fLim1` K)` ((Y FilMap ((nei` J)` {A}))` G))) -> (G` A) e. ((fLim1` K)` ((Y FilMap F)` G)))
82	53, 56, 59, 74, 78, 81	syl311anc 1114	1 |- (((J e. Top /\ K e. Top /\ F e. fBas) /\ (G e. ((J CnP K)` A) /\ A e. ((fLim1` J)` (filGen` F)) /\ X = U.F)) -> (G` A) e. ((fLim1` K)` ((Y FilMap F)` G)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  _Vcvv 2292   C_ wss 2593  (/)c0 2875  {csn 3044  U.cuni 3177  -->wf 3994  ` cfv 3998  (class class class)co 4884  Topctop 8857  neicnei 8988   CnP ccnp 9029  fBascfbas 10257  filGencfg 10258  Filcfil 10264  fLim1cflim1 10294   FilMap cfilmap 10304

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-opr 4886  df-oprab 4887  df-map 5383  df-top 8861  df-nei 8989  df-cnp 9031  df-fbas 10259  df-fg 10260  df-fil 10265  df-flim1 10295  df-filmap 10306  df-flimf 10316

Copyright terms: Public domain