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 ⊢ 𝐶 = ∪ 𝐽
flfcntr.b ⊢ 𝐵 = ∪ 𝐾
flfcntr.j ⊢ ( 𝜑 → 𝐽 ∈ Top )
flfcntr.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
flfcntr.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) )
flfcntr.y ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion flfcntr ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 flfcntr.c ⊢ 𝐶 = ∪ 𝐽
2 flfcntr.b ⊢ 𝐵 = ∪ 𝐾
3 flfcntr.j ⊢ ( 𝜑 → 𝐽 ∈ Top )
4 flfcntr.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
5 flfcntr.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) )
6 flfcntr.y ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
7 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
8 7 eleq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ↔ ( 𝐹 ‘ 𝑋 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
9 oveq2 ⊢ ( 𝑎 = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) → ( ( 𝐽 ↾t 𝐴 ) fLim 𝑎 ) = ( ( 𝐽 ↾t 𝐴 ) fLim ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) )
10 oveq2 ⊢ ( 𝑎 = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) → ( 𝐾 fLimf 𝑎 ) = ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) )
11 10 fveq1d ⊢ ( 𝑎 = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) → ( ( 𝐾 fLimf 𝑎 ) ‘ 𝐹 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
12 11 eleq2d ⊢ ( 𝑎 = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑎 ) ‘ 𝐹 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
13 9 12 raleqbidv ⊢ ( 𝑎 = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) → ( ∀ 𝑥 ∈ ( ( 𝐽 ↾t 𝐴 ) fLim 𝑎 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑎 ) ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ ( ( 𝐽 ↾t 𝐴 ) fLim ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) )
14 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
15 3 14 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐶 ) )
16 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
17 15 4 16 syl2anc ⊢ ( 𝜑 → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
18 cntop2 ⊢ ( 𝐹 ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) → 𝐾 ∈ Top )
19 5 18 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
20 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
21 19 20 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝐵 ) )
22 cnflf ⊢ ( ( ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝐵 ) ) → ( 𝐹 ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑎 ∈ ( Fil ‘ 𝐴 ) ∀ 𝑥 ∈ ( ( 𝐽 ↾t 𝐴 ) fLim 𝑎 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑎 ) ‘ 𝐹 ) ) ) )
23 17 21 22 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑎 ∈ ( Fil ‘ 𝐴 ) ∀ 𝑥 ∈ ( ( 𝐽 ↾t 𝐴 ) fLim 𝑎 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑎 ) ‘ 𝐹 ) ) ) )
24 5 23 mpbid ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑎 ∈ ( Fil ‘ 𝐴 ) ∀ 𝑥 ∈ ( ( 𝐽 ↾t 𝐴 ) fLim 𝑎 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑎 ) ‘ 𝐹 ) ) )
25 24 simprd ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( Fil ‘ 𝐴 ) ∀ 𝑥 ∈ ( ( 𝐽 ↾t 𝐴 ) fLim 𝑎 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑎 ) ‘ 𝐹 ) )
26 1 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶 ) → 𝐴 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
27 3 4 26 syl2anc ⊢ ( 𝜑 → 𝐴 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
28 27 6 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
29 4 6 sseldd ⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
30 trnei ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑋 ∈ 𝐶 ) → ( 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
31 15 4 29 30 syl3anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) )
32 28 31 mpbid ⊢ ( 𝜑 → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) )
33 13 25 32 rspcdva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝐽 ↾t 𝐴 ) fLim ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )
34 neiflim ⊢ ( ( ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( ( 𝐽 ↾t 𝐴 ) fLim ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑋 } ) ) )
35 17 6 34 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐽 ↾t 𝐴 ) fLim ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑋 } ) ) )
36 6 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐴 )
37 1 neitr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶 ∧ { 𝑋 } ⊆ 𝐴 ) → ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑋 } ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) )
38 3 4 36 37 syl3anc ⊢ ( 𝜑 → ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑋 } ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) )
39 38 oveq2d ⊢ ( 𝜑 → ( ( 𝐽 ↾t 𝐴 ) fLim ( ( nei ‘ ( 𝐽 ↾t 𝐴 ) ) ‘ { 𝑋 } ) ) = ( ( 𝐽 ↾t 𝐴 ) fLim ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) )
40 35 39 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐽 ↾t 𝐴 ) fLim ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) )
41 8 33 40 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑋 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) )