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=J
flfcntr.b B=K
flfcntr.j φJTop
flfcntr.a φAC
flfcntr.1 φFJ𝑡ACnK
flfcntr.y φXA
Assertion flfcntr φFXKfLimfneiJX𝑡AF

Proof

Step Hyp Ref Expression
1 flfcntr.c C=J
2 flfcntr.b B=K
3 flfcntr.j φJTop
4 flfcntr.a φAC
5 flfcntr.1 φFJ𝑡ACnK
6 flfcntr.y φXA
7 fveq2 x=XFx=FX
8 7 eleq1d x=XFxKfLimfneiJX𝑡AFFXKfLimfneiJX𝑡AF
9 oveq2 a=neiJX𝑡AJ𝑡AfLima=J𝑡AfLimneiJX𝑡A
10 oveq2 a=neiJX𝑡AKfLimfa=KfLimfneiJX𝑡A
11 10 fveq1d a=neiJX𝑡AKfLimfaF=KfLimfneiJX𝑡AF
12 11 eleq2d a=neiJX𝑡AFxKfLimfaFFxKfLimfneiJX𝑡AF
13 9 12 raleqbidv a=neiJX𝑡AxJ𝑡AfLimaFxKfLimfaFxJ𝑡AfLimneiJX𝑡AFxKfLimfneiJX𝑡AF
14 1 toptopon JTopJTopOnC
15 3 14 sylib φJTopOnC
16 resttopon JTopOnCACJ𝑡ATopOnA
17 15 4 16 syl2anc φJ𝑡ATopOnA
18 cntop2 FJ𝑡ACnKKTop
19 5 18 syl φKTop
20 2 toptopon KTopKTopOnB
21 19 20 sylib φKTopOnB
22 cnflf J𝑡ATopOnAKTopOnBFJ𝑡ACnKF:ABaFilAxJ𝑡AfLimaFxKfLimfaF
23 17 21 22 syl2anc φFJ𝑡ACnKF:ABaFilAxJ𝑡AfLimaFxKfLimfaF
24 5 23 mpbid φF:ABaFilAxJ𝑡AfLimaFxKfLimfaF
25 24 simprd φaFilAxJ𝑡AfLimaFxKfLimfaF
26 1 sscls JTopACAclsJA
27 3 4 26 syl2anc φAclsJA
28 27 6 sseldd φXclsJA
29 4 6 sseldd φXC
30 trnei JTopOnCACXCXclsJAneiJX𝑡AFilA
31 15 4 29 30 syl3anc φXclsJAneiJX𝑡AFilA
32 28 31 mpbid φneiJX𝑡AFilA
33 13 25 32 rspcdva φxJ𝑡AfLimneiJX𝑡AFxKfLimfneiJX𝑡AF
34 neiflim J𝑡ATopOnAXAXJ𝑡AfLimneiJ𝑡AX
35 17 6 34 syl2anc φXJ𝑡AfLimneiJ𝑡AX
36 6 snssd φXA
37 1 neitr JTopACXAneiJ𝑡AX=neiJX𝑡A
38 3 4 36 37 syl3anc φneiJ𝑡AX=neiJX𝑡A
39 38 oveq2d φJ𝑡AfLimneiJ𝑡AX=J𝑡AfLimneiJX𝑡A
40 35 39 eleqtrd φXJ𝑡AfLimneiJX𝑡A
41 8 33 40 rspcdva φFXKfLimfneiJX𝑡AF