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 = U. J
flfcntr.b 
|- B = U. K
flfcntr.j 
|- ( ph -> J e. Top )
flfcntr.a 
|- ( ph -> A C_ C )
flfcntr.1 
|- ( ph -> F e. ( ( J |`t A ) Cn K ) )
flfcntr.y 
|- ( ph -> X e. A )
Assertion flfcntr 
|- ( ph -> ( F ` X ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) )

Proof

Step Hyp Ref Expression
1 flfcntr.c 
 |-  C = U. J
2 flfcntr.b 
 |-  B = U. K
3 flfcntr.j 
 |-  ( ph -> J e. Top )
4 flfcntr.a 
 |-  ( ph -> A C_ C )
5 flfcntr.1 
 |-  ( ph -> F e. ( ( J |`t A ) Cn K ) )
6 flfcntr.y 
 |-  ( ph -> X e. A )
7 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
8 7 eleq1d 
 |-  ( x = X -> ( ( F ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) <-> ( F ` X ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ) )
9 oveq2 
 |-  ( a = ( ( ( nei ` J ) ` { X } ) |`t A ) -> ( ( J |`t A ) fLim a ) = ( ( J |`t A ) fLim ( ( ( nei ` J ) ` { X } ) |`t A ) ) )
10 oveq2 
 |-  ( a = ( ( ( nei ` J ) ` { X } ) |`t A ) -> ( K fLimf a ) = ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) )
11 10 fveq1d 
 |-  ( a = ( ( ( nei ` J ) ` { X } ) |`t A ) -> ( ( K fLimf a ) ` F ) = ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) )
12 11 eleq2d 
 |-  ( a = ( ( ( nei ` J ) ` { X } ) |`t A ) -> ( ( F ` x ) e. ( ( K fLimf a ) ` F ) <-> ( F ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ) )
13 9 12 raleqbidv 
 |-  ( a = ( ( ( nei ` J ) ` { X } ) |`t A ) -> ( A. x e. ( ( J |`t A ) fLim a ) ( F ` x ) e. ( ( K fLimf a ) ` F ) <-> A. x e. ( ( J |`t A ) fLim ( ( ( nei ` J ) ` { X } ) |`t A ) ) ( F ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) ) )
14 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` C ) )
15 3 14 sylib 
 |-  ( ph -> J e. ( TopOn ` C ) )
16 resttopon 
 |-  ( ( J e. ( TopOn ` C ) /\ A C_ C ) -> ( J |`t A ) e. ( TopOn ` A ) )
17 15 4 16 syl2anc 
 |-  ( ph -> ( J |`t A ) e. ( TopOn ` A ) )
18 cntop2 
 |-  ( F e. ( ( J |`t A ) Cn K ) -> K e. Top )
19 5 18 syl 
 |-  ( ph -> K e. Top )
20 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` B ) )
21 19 20 sylib 
 |-  ( ph -> K e. ( TopOn ` B ) )
22 cnflf 
 |-  ( ( ( J |`t A ) e. ( TopOn ` A ) /\ K e. ( TopOn ` B ) ) -> ( F e. ( ( J |`t A ) Cn K ) <-> ( F : A --> B /\ A. a e. ( Fil ` A ) A. x e. ( ( J |`t A ) fLim a ) ( F ` x ) e. ( ( K fLimf a ) ` F ) ) ) )
23 17 21 22 syl2anc 
 |-  ( ph -> ( F e. ( ( J |`t A ) Cn K ) <-> ( F : A --> B /\ A. a e. ( Fil ` A ) A. x e. ( ( J |`t A ) fLim a ) ( F ` x ) e. ( ( K fLimf a ) ` F ) ) ) )
24 5 23 mpbid 
 |-  ( ph -> ( F : A --> B /\ A. a e. ( Fil ` A ) A. x e. ( ( J |`t A ) fLim a ) ( F ` x ) e. ( ( K fLimf a ) ` F ) ) )
25 24 simprd 
 |-  ( ph -> A. a e. ( Fil ` A ) A. x e. ( ( J |`t A ) fLim a ) ( F ` x ) e. ( ( K fLimf a ) ` F ) )
26 1 sscls 
 |-  ( ( J e. Top /\ A C_ C ) -> A C_ ( ( cls ` J ) ` A ) )
27 3 4 26 syl2anc 
 |-  ( ph -> A C_ ( ( cls ` J ) ` A ) )
28 27 6 sseldd 
 |-  ( ph -> X e. ( ( cls ` J ) ` A ) )
29 4 6 sseldd 
 |-  ( ph -> X e. C )
30 trnei 
 |-  ( ( J e. ( TopOn ` C ) /\ A C_ C /\ X e. C ) -> ( X e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { X } ) |`t A ) e. ( Fil ` A ) ) )
31 15 4 29 30 syl3anc 
 |-  ( ph -> ( X e. ( ( cls ` J ) ` A ) <-> ( ( ( nei ` J ) ` { X } ) |`t A ) e. ( Fil ` A ) ) )
32 28 31 mpbid 
 |-  ( ph -> ( ( ( nei ` J ) ` { X } ) |`t A ) e. ( Fil ` A ) )
33 13 25 32 rspcdva 
 |-  ( ph -> A. x e. ( ( J |`t A ) fLim ( ( ( nei ` J ) ` { X } ) |`t A ) ) ( F ` x ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) )
34 neiflim 
 |-  ( ( ( J |`t A ) e. ( TopOn ` A ) /\ X e. A ) -> X e. ( ( J |`t A ) fLim ( ( nei ` ( J |`t A ) ) ` { X } ) ) )
35 17 6 34 syl2anc 
 |-  ( ph -> X e. ( ( J |`t A ) fLim ( ( nei ` ( J |`t A ) ) ` { X } ) ) )
36 6 snssd 
 |-  ( ph -> { X } C_ A )
37 1 neitr 
 |-  ( ( J e. Top /\ A C_ C /\ { X } C_ A ) -> ( ( nei ` ( J |`t A ) ) ` { X } ) = ( ( ( nei ` J ) ` { X } ) |`t A ) )
38 3 4 36 37 syl3anc 
 |-  ( ph -> ( ( nei ` ( J |`t A ) ) ` { X } ) = ( ( ( nei ` J ) ` { X } ) |`t A ) )
39 38 oveq2d 
 |-  ( ph -> ( ( J |`t A ) fLim ( ( nei ` ( J |`t A ) ) ` { X } ) ) = ( ( J |`t A ) fLim ( ( ( nei ` J ) ` { X } ) |`t A ) ) )
40 35 39 eleqtrd 
 |-  ( ph -> X e. ( ( J |`t A ) fLim ( ( ( nei ` J ) ` { X } ) |`t A ) ) )
41 8 33 40 rspcdva 
 |-  ( ph -> ( F ` X ) e. ( ( K fLimf ( ( ( nei ` J ) ` { X } ) |`t A ) ) ` F ) )