# Metamath Proof Explorer

## Theorem flfcntr

Description: A continuous function's value is always in the trace of its filter limit. (Contributed by Thierry Arnoux, 30-Aug-2020)

Ref Expression
Hypotheses flfcntr.c ${⊢}{C}=\bigcup {J}$
flfcntr.b ${⊢}{B}=\bigcup {K}$
flfcntr.j ${⊢}{\phi }\to {J}\in \mathrm{Top}$
flfcntr.a ${⊢}{\phi }\to {A}\subseteq {C}$
flfcntr.1 ${⊢}{\phi }\to {F}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{Cn}{K}\right)$
flfcntr.y ${⊢}{\phi }\to {X}\in {A}$
Assertion flfcntr ${⊢}{\phi }\to {F}\left({X}\right)\in \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)$

### Proof

Step Hyp Ref Expression
1 flfcntr.c ${⊢}{C}=\bigcup {J}$
2 flfcntr.b ${⊢}{B}=\bigcup {K}$
3 flfcntr.j ${⊢}{\phi }\to {J}\in \mathrm{Top}$
4 flfcntr.a ${⊢}{\phi }\to {A}\subseteq {C}$
5 flfcntr.1 ${⊢}{\phi }\to {F}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{Cn}{K}\right)$
6 flfcntr.y ${⊢}{\phi }\to {X}\in {A}$
7 fveq2 ${⊢}{x}={X}\to {F}\left({x}\right)={F}\left({X}\right)$
8 7 eleq1d ${⊢}{x}={X}\to \left({F}\left({x}\right)\in \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)↔{F}\left({X}\right)\in \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\right)$
9 oveq2 ${⊢}{a}=\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\to \left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}{a}=\left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)$
10 oveq2 ${⊢}{a}=\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\to {K}\mathrm{fLimf}{a}={K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)$
11 10 fveq1d ${⊢}{a}=\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\to \left({K}\mathrm{fLimf}{a}\right)\left({F}\right)=\left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)$
12 11 eleq2d ${⊢}{a}=\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\to \left({F}\left({x}\right)\in \left({K}\mathrm{fLimf}{a}\right)\left({F}\right)↔{F}\left({x}\right)\in \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\right)$
13 9 12 raleqbidv ${⊢}{a}=\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\to \left(\forall {x}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}{a}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left({K}\mathrm{fLimf}{a}\right)\left({F}\right)↔\forall {x}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)\right)$
14 1 toptopon ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left({C}\right)$
15 3 14 sylib ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({C}\right)$
16 resttopon ${⊢}\left({J}\in \mathrm{TopOn}\left({C}\right)\wedge {A}\subseteq {C}\right)\to {J}{↾}_{𝑡}{A}\in \mathrm{TopOn}\left({A}\right)$
17 15 4 16 syl2anc ${⊢}{\phi }\to {J}{↾}_{𝑡}{A}\in \mathrm{TopOn}\left({A}\right)$
18 cntop2 ${⊢}{F}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{Cn}{K}\right)\to {K}\in \mathrm{Top}$
19 5 18 syl ${⊢}{\phi }\to {K}\in \mathrm{Top}$
20 2 toptopon ${⊢}{K}\in \mathrm{Top}↔{K}\in \mathrm{TopOn}\left({B}\right)$
21 19 20 sylib ${⊢}{\phi }\to {K}\in \mathrm{TopOn}\left({B}\right)$
22 cnflf ${⊢}\left({J}{↾}_{𝑡}{A}\in \mathrm{TopOn}\left({A}\right)\wedge {K}\in \mathrm{TopOn}\left({B}\right)\right)\to \left({F}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{Cn}{K}\right)↔\left({F}:{A}⟶{B}\wedge \forall {a}\in \mathrm{Fil}\left({A}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}{a}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left({K}\mathrm{fLimf}{a}\right)\left({F}\right)\right)\right)$
23 17 21 22 syl2anc ${⊢}{\phi }\to \left({F}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{Cn}{K}\right)↔\left({F}:{A}⟶{B}\wedge \forall {a}\in \mathrm{Fil}\left({A}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}{a}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left({K}\mathrm{fLimf}{a}\right)\left({F}\right)\right)\right)$
24 5 23 mpbid ${⊢}{\phi }\to \left({F}:{A}⟶{B}\wedge \forall {a}\in \mathrm{Fil}\left({A}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}{a}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left({K}\mathrm{fLimf}{a}\right)\left({F}\right)\right)$
25 24 simprd ${⊢}{\phi }\to \forall {a}\in \mathrm{Fil}\left({A}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}{a}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left({K}\mathrm{fLimf}{a}\right)\left({F}\right)$
26 1 sscls ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\subseteq {C}\right)\to {A}\subseteq \mathrm{cls}\left({J}\right)\left({A}\right)$
27 3 4 26 syl2anc ${⊢}{\phi }\to {A}\subseteq \mathrm{cls}\left({J}\right)\left({A}\right)$
28 27 6 sseldd ${⊢}{\phi }\to {X}\in \mathrm{cls}\left({J}\right)\left({A}\right)$
29 4 6 sseldd ${⊢}{\phi }\to {X}\in {C}$
30 trnei ${⊢}\left({J}\in \mathrm{TopOn}\left({C}\right)\wedge {A}\subseteq {C}\wedge {X}\in {C}\right)\to \left({X}\in \mathrm{cls}\left({J}\right)\left({A}\right)↔\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\in \mathrm{Fil}\left({A}\right)\right)$
31 15 4 29 30 syl3anc ${⊢}{\phi }\to \left({X}\in \mathrm{cls}\left({J}\right)\left({A}\right)↔\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\in \mathrm{Fil}\left({A}\right)\right)$
32 28 31 mpbid ${⊢}{\phi }\to \mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\in \mathrm{Fil}\left({A}\right)$
33 13 25 32 rspcdva ${⊢}{\phi }\to \forall {x}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)$
34 neiflim ${⊢}\left({J}{↾}_{𝑡}{A}\in \mathrm{TopOn}\left({A}\right)\wedge {X}\in {A}\right)\to {X}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}\mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{X}\right\}\right)\right)$
35 17 6 34 syl2anc ${⊢}{\phi }\to {X}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}\mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{X}\right\}\right)\right)$
36 6 snssd ${⊢}{\phi }\to \left\{{X}\right\}\subseteq {A}$
37 1 neitr ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\subseteq {C}\wedge \left\{{X}\right\}\subseteq {A}\right)\to \mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{X}\right\}\right)=\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}$
38 3 4 36 37 syl3anc ${⊢}{\phi }\to \mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{X}\right\}\right)=\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}$
39 38 oveq2d ${⊢}{\phi }\to \left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}\mathrm{nei}\left({J}{↾}_{𝑡}{A}\right)\left(\left\{{X}\right\}\right)=\left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)$
40 35 39 eleqtrd ${⊢}{\phi }\to {X}\in \left(\left({J}{↾}_{𝑡}{A}\right)\mathrm{fLim}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)\right)$
41 8 33 40 rspcdva ${⊢}{\phi }\to {F}\left({X}\right)\in \left({K}\mathrm{fLimf}\left(\mathrm{nei}\left({J}\right)\left(\left\{{X}\right\}\right){↾}_{𝑡}{A}\right)\right)\left({F}\right)$