Theorem cnpfcfi 24306

Description: Lemma for cnpfcf 24307. If a function is continuous at a point, it respects clustering there. (Contributed by Jeff Hankins, 20-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)

Assertion

Ref	Expression
cnpfcfi	⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝐿)‘𝐹))

Proof of Theorem cnpfcfi

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp2 1155	. . 3 ⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐴 ∈ (𝐽 fClus 𝐿))
2		eqid 2760	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
3	2	fclsfil 24276	. . . . 5 ⊢ (𝐴 ∈ (𝐽 fClus 𝐿) → 𝐿 ∈ (Fil‘∪ 𝐽))
4	3	3ad2ant2 1152	. . . 4 ⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐿 ∈ (Fil‘∪ 𝐽))
5		fclsfnflim 24293	. . . 4 ⊢ (𝐿 ∈ (Fil‘∪ 𝐽) → (𝐴 ∈ (𝐽 fClus 𝐿) ↔ ∃𝑓 ∈ (Fil‘∪ 𝐽)(𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓))))
6	4, 5	syl 18	. . 3 ⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐴 ∈ (𝐽 fClus 𝐿) ↔ ∃𝑓 ∈ (Fil‘∪ 𝐽)(𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓))))
7	1, 6	mpbid 235	. 2 ⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∃𝑓 ∈ (Fil‘∪ 𝐽)(𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))
8		simpl1 1210	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐾 ∈ Top)
9		toptopon2 23183	. . . . . 6 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾))
10	8, 9	sylib 221	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐾 ∈ (TopOn‘∪ 𝐾))
11		simprl 783	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝑓 ∈ (Fil‘∪ 𝐽))
12		eqid 2760	. . . . . . . 8 ⊢ ∪ 𝐾 = ∪ 𝐾
13	2, 12	cnpf 23512	. . . . . . 7 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → 𝐹:∪ 𝐽⟶∪ 𝐾)
14	13	3ad2ant3 1153	. . . . . 6 ⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:∪ 𝐽⟶∪ 𝐾)
15	14	adantr 486	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐹:∪ 𝐽⟶∪ 𝐾)
16		flfssfcf 24304	. . . . 5 ⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾) ∧ 𝑓 ∈ (Fil‘∪ 𝐽) ∧ 𝐹:∪ 𝐽⟶∪ 𝐾) → ((𝐾 fLimf 𝑓)‘𝐹) ⊆ ((𝐾 fClusf 𝑓)‘𝐹))
17	10, 11, 15, 16	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fLimf 𝑓)‘𝐹) ⊆ ((𝐾 fClusf 𝑓)‘𝐹))
18	12	topopn 23171	. . . . . . . 8 ⊢ (𝐾 ∈ Top → ∪ 𝐾 ∈ 𝐾)
19	8, 18	syl 18	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ∪ 𝐾 ∈ 𝐾)
20	4	adantr 486	. . . . . . . 8 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐿 ∈ (Fil‘∪ 𝐽))
21		filfbas 24114	. . . . . . . 8 ⊢ (𝐿 ∈ (Fil‘∪ 𝐽) → 𝐿 ∈ (fBas‘∪ 𝐽))
22	20, 21	syl 18	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐿 ∈ (fBas‘∪ 𝐽))
23		fmfil 24210	. . . . . . 7 ⊢ ((∪ 𝐾 ∈ 𝐾 ∧ 𝐿 ∈ (fBas‘∪ 𝐽) ∧ 𝐹:∪ 𝐽⟶∪ 𝐾) → ((∪ 𝐾 FilMap 𝐹)‘𝐿) ∈ (Fil‘∪ 𝐾))
24	19, 22, 15, 23	syl3anc 1398	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((∪ 𝐾 FilMap 𝐹)‘𝐿) ∈ (Fil‘∪ 𝐾))
25		filfbas 24114	. . . . . . . 8 ⊢ (𝑓 ∈ (Fil‘∪ 𝐽) → 𝑓 ∈ (fBas‘∪ 𝐽))
26	25	ad2antrl 741	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝑓 ∈ (fBas‘∪ 𝐽))
27		simprrl 793	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐿 ⊆ 𝑓)
28		fmss 24212	. . . . . . 7 ⊢ (((∪ 𝐾 ∈ 𝐾 ∧ 𝐿 ∈ (fBas‘∪ 𝐽) ∧ 𝑓 ∈ (fBas‘∪ 𝐽)) ∧ (𝐹:∪ 𝐽⟶∪ 𝐾 ∧ 𝐿 ⊆ 𝑓)) → ((∪ 𝐾 FilMap 𝐹)‘𝐿) ⊆ ((∪ 𝐾 FilMap 𝐹)‘𝑓))
29	19, 22, 26, 15, 27, 28	syl32anc 1405	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((∪ 𝐾 FilMap 𝐹)‘𝐿) ⊆ ((∪ 𝐾 FilMap 𝐹)‘𝑓))
30		fclsss2 24289	. . . . . 6 ⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾) ∧ ((∪ 𝐾 FilMap 𝐹)‘𝐿) ∈ (Fil‘∪ 𝐾) ∧ ((∪ 𝐾 FilMap 𝐹)‘𝐿) ⊆ ((∪ 𝐾 FilMap 𝐹)‘𝑓)) → (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝑓)) ⊆ (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝐿)))
31	10, 24, 29, 30	syl3anc 1398	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝑓)) ⊆ (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝐿)))
32		fcfval 24299	. . . . . 6 ⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾) ∧ 𝑓 ∈ (Fil‘∪ 𝐽) ∧ 𝐹:∪ 𝐽⟶∪ 𝐾) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝑓)))
33	10, 11, 15, 32	syl3anc 1398	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝑓)))
34		fcfval 24299	. . . . . 6 ⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾) ∧ 𝐿 ∈ (Fil‘∪ 𝐽) ∧ 𝐹:∪ 𝐽⟶∪ 𝐾) → ((𝐾 fClusf 𝐿)‘𝐹) = (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝐿)))
35	10, 20, 15, 34	syl3anc 1398	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fClusf 𝐿)‘𝐹) = (𝐾 fClus ((∪ 𝐾 FilMap 𝐹)‘𝐿)))
36	31, 33, 35	3sstr4d 3986	. . . 4 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) ⊆ ((𝐾 fClusf 𝐿)‘𝐹))
37	17, 36	sstrd 3941	. . 3 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → ((𝐾 fLimf 𝑓)‘𝐹) ⊆ ((𝐾 fClusf 𝐿)‘𝐹))
38		simprrr 794	. . . 4 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐴 ∈ (𝐽 fLim 𝑓))
39		simpl3 1212	. . . 4 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴))
40		cnpflfi 24265	. . . 4 ⊢ ((𝐴 ∈ (𝐽 fLim 𝑓) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑓)‘𝐹))
41	38, 39, 40	syl2anc 596	. . 3 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑓)‘𝐹))
42	37, 41	sseldd 3932	. 2 ⊢ (((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) ∧ (𝑓 ∈ (Fil‘∪ 𝐽) ∧ (𝐿 ⊆ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓)))) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝐿)‘𝐹))
43	7, 42	rexlimddv 3169	1 ⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝐿)‘𝐹))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∃wrex 3086   ⊆ wss 3899  ∪ cuni 4867  ⟶wf 6524  ‘cfv 6528  (class class class)co 7409  fBascfbas 21613  Topctop 23158  TopOnctopon 23175   CnP ccnp 23490  Filcfil 24111   FilMap cfm 24199   fLim cflim 24200   fLimf cflf 24201   fClus cfcls 24202   fClusf cfcf 24203

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7862  df-1st 7985  df-2nd 7986  df-1o 8455  df-2o 8456  df-map 8828  df-en 8953  df-fin 8956  df-fi 9381  df-fbas 21622  df-fg 21623  df-top 23159  df-topon 23176  df-cld 23284  df-ntr 23285  df-cls 23286  df-nei 23363  df-cnp 23493  df-fil 24112  df-fm 24204  df-flim 24205  df-flf 24206  df-fcls 24207  df-fcf 24208

This theorem is used by:  cnpfcf  24307