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 ⊢ φ → J ∈ Top
flfcntr.a ⊢ φ → A ⊆ C
flfcntr.1 ⊢ φ → F ∈ J ↾ 𝑡 A Cn K
flfcntr.y ⊢ φ → X ∈ A
Assertion flfcntr ⊢ φ → F ⁡ X ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F

Proof

Step Hyp Ref Expression
1 flfcntr.c ⊢ C = ⋃ J
2 flfcntr.b ⊢ B = ⋃ K
3 flfcntr.j ⊢ φ → J ∈ Top
4 flfcntr.a ⊢ φ → A ⊆ C
5 flfcntr.1 ⊢ φ → F ∈ J ↾ 𝑡 A Cn K
6 flfcntr.y ⊢ φ → X ∈ A
7 fveq2 ⊢ x = X → F ⁡ x = F ⁡ X
8 7 eleq1d ⊢ x = X → F ⁡ x ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F ↔ F ⁡ X ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
9 oveq2 ⊢ a = nei ⁡ J ⁡ X ↾ 𝑡 A → J ↾ 𝑡 A fLim a = J ↾ 𝑡 A fLim nei ⁡ J ⁡ X ↾ 𝑡 A
10 oveq2 ⊢ a = nei ⁡ J ⁡ X ↾ 𝑡 A → K fLimf a = K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A
11 10 fveq1d ⊢ a = nei ⁡ J ⁡ X ↾ 𝑡 A → K fLimf a ⁡ F = K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
12 11 eleq2d ⊢ a = nei ⁡ J ⁡ X ↾ 𝑡 A → F ⁡ x ∈ K fLimf a ⁡ F ↔ F ⁡ x ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
13 9 12 raleqbidv ⊢ a = nei ⁡ J ⁡ X ↾ 𝑡 A → ∀ x ∈ J ↾ 𝑡 A fLim a F ⁡ x ∈ K fLimf a ⁡ F ↔ ∀ x ∈ J ↾ 𝑡 A fLim nei ⁡ J ⁡ X ↾ 𝑡 A F ⁡ x ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
14 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ C
15 3 14 sylib ⊢ φ → J ∈ TopOn ⁡ C
16 resttopon ⊢ J ∈ TopOn ⁡ C ∧ A ⊆ C → J ↾ 𝑡 A ∈ TopOn ⁡ A
17 15 4 16 syl2anc ⊢ φ → J ↾ 𝑡 A ∈ TopOn ⁡ A
18 cntop2 ⊢ F ∈ J ↾ 𝑡 A Cn K → K ∈ Top
19 5 18 syl ⊢ φ → K ∈ Top
20 2 toptopon ⊢ K ∈ Top ↔ K ∈ TopOn ⁡ B
21 19 20 sylib ⊢ φ → K ∈ TopOn ⁡ B
22 cnflf ⊢ J ↾ 𝑡 A ∈ TopOn ⁡ A ∧ K ∈ TopOn ⁡ B → F ∈ J ↾ 𝑡 A Cn K ↔ F : A ⟶ B ∧ ∀ a ∈ Fil ⁡ A ∀ x ∈ J ↾ 𝑡 A fLim a F ⁡ x ∈ K fLimf a ⁡ F
23 17 21 22 syl2anc ⊢ φ → F ∈ J ↾ 𝑡 A Cn K ↔ F : A ⟶ B ∧ ∀ a ∈ Fil ⁡ A ∀ x ∈ J ↾ 𝑡 A fLim a F ⁡ x ∈ K fLimf a ⁡ F
24 5 23 mpbid ⊢ φ → F : A ⟶ B ∧ ∀ a ∈ Fil ⁡ A ∀ x ∈ J ↾ 𝑡 A fLim a F ⁡ x ∈ K fLimf a ⁡ F
25 24 simprd ⊢ φ → ∀ a ∈ Fil ⁡ A ∀ x ∈ J ↾ 𝑡 A fLim a F ⁡ x ∈ K fLimf a ⁡ F
26 1 sscls ⊢ J ∈ Top ∧ A ⊆ C → A ⊆ cls ⁡ J ⁡ A
27 3 4 26 syl2anc ⊢ φ → A ⊆ cls ⁡ J ⁡ A
28 27 6 sseldd ⊢ φ → X ∈ cls ⁡ J ⁡ A
29 4 6 sseldd ⊢ φ → X ∈ C
30 trnei ⊢ J ∈ TopOn ⁡ C ∧ A ⊆ C ∧ X ∈ C → X ∈ cls ⁡ J ⁡ A ↔ nei ⁡ J ⁡ X ↾ 𝑡 A ∈ Fil ⁡ A
31 15 4 29 30 syl3anc ⊢ φ → X ∈ cls ⁡ J ⁡ A ↔ nei ⁡ J ⁡ X ↾ 𝑡 A ∈ Fil ⁡ A
32 28 31 mpbid ⊢ φ → nei ⁡ J ⁡ X ↾ 𝑡 A ∈ Fil ⁡ A
33 13 25 32 rspcdva ⊢ φ → ∀ x ∈ J ↾ 𝑡 A fLim nei ⁡ J ⁡ X ↾ 𝑡 A F ⁡ x ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F
34 neiflim ⊢ J ↾ 𝑡 A ∈ TopOn ⁡ A ∧ X ∈ A → X ∈ J ↾ 𝑡 A fLim nei ⁡ J ↾ 𝑡 A ⁡ X
35 17 6 34 syl2anc ⊢ φ → X ∈ J ↾ 𝑡 A fLim nei ⁡ J ↾ 𝑡 A ⁡ X
36 6 snssd ⊢ φ → X ⊆ A
37 1 neitr ⊢ J ∈ Top ∧ A ⊆ C ∧ X ⊆ A → nei ⁡ J ↾ 𝑡 A ⁡ X = nei ⁡ J ⁡ X ↾ 𝑡 A
38 3 4 36 37 syl3anc ⊢ φ → nei ⁡ J ↾ 𝑡 A ⁡ X = nei ⁡ J ⁡ X ↾ 𝑡 A
39 38 oveq2d ⊢ φ → J ↾ 𝑡 A fLim nei ⁡ J ↾ 𝑡 A ⁡ X = J ↾ 𝑡 A fLim nei ⁡ J ⁡ X ↾ 𝑡 A
40 35 39 eleqtrd ⊢ φ → X ∈ J ↾ 𝑡 A fLim nei ⁡ J ⁡ X ↾ 𝑡 A
41 8 33 40 rspcdva ⊢ φ → F ⁡ X ∈ K fLimf nei ⁡ J ⁡ X ↾ 𝑡 A ⁡ F