Step | Hyp | Ref
| Expression |
1 | | flfcntr.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) |
2 | | flfcntr.j |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ Top) |
3 | | flfcntr.c |
. . . . . . . . 9
⊢ 𝐶 = ∪
𝐽 |
4 | 3 | toptopon 20722 |
. . . . . . . 8
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶)) |
5 | 2, 4 | sylib 208 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐶)) |
6 | | flfcntr.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
7 | | resttopon 20965 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴)) |
8 | 5, 6, 7 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴)) |
9 | | cntop2 21045 |
. . . . . . . 8
⊢ (𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) → 𝐾 ∈ Top) |
10 | 1, 9 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) |
11 | | flfcntr.b |
. . . . . . . 8
⊢ 𝐵 = ∪
𝐾 |
12 | 11 | toptopon 20722 |
. . . . . . 7
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵)) |
13 | 10, 12 | sylib 208 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐵)) |
14 | | cnflf 21806 |
. . . . . 6
⊢ (((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) ∧ 𝐾 ∈ (TopOn‘𝐵)) → (𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑎 ∈ (Fil‘𝐴)∀𝑥 ∈ ((𝐽 ↾t 𝐴) fLim 𝑎)(𝐹‘𝑥) ∈ ((𝐾 fLimf 𝑎)‘𝐹)))) |
15 | 8, 13, 14 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑎 ∈ (Fil‘𝐴)∀𝑥 ∈ ((𝐽 ↾t 𝐴) fLim 𝑎)(𝐹‘𝑥) ∈ ((𝐾 fLimf 𝑎)‘𝐹)))) |
16 | 1, 15 | mpbid 222 |
. . . 4
⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ∧ ∀𝑎 ∈ (Fil‘𝐴)∀𝑥 ∈ ((𝐽 ↾t 𝐴) fLim 𝑎)(𝐹‘𝑥) ∈ ((𝐾 fLimf 𝑎)‘𝐹))) |
17 | 16 | simprd 479 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ (Fil‘𝐴)∀𝑥 ∈ ((𝐽 ↾t 𝐴) fLim 𝑎)(𝐹‘𝑥) ∈ ((𝐾 fLimf 𝑎)‘𝐹)) |
18 | 3 | sscls 20860 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶) → 𝐴 ⊆ ((cls‘𝐽)‘𝐴)) |
19 | 2, 6, 18 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ((cls‘𝐽)‘𝐴)) |
20 | | flfcntr.y |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
21 | 19, 20 | sseldd 3604 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ((cls‘𝐽)‘𝐴)) |
22 | 6, 20 | sseldd 3604 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐶) |
23 | | trnei 21696 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑋 ∈ 𝐶) → (𝑋 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑋}) ↾t 𝐴) ∈ (Fil‘𝐴))) |
24 | 5, 6, 22, 23 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (𝑋 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑋}) ↾t 𝐴) ∈ (Fil‘𝐴))) |
25 | 21, 24 | mpbid 222 |
. . . 4
⊢ (𝜑 → (((nei‘𝐽)‘{𝑋}) ↾t 𝐴) ∈ (Fil‘𝐴)) |
26 | | oveq2 6658 |
. . . . . 6
⊢ (𝑎 = (((nei‘𝐽)‘{𝑋}) ↾t 𝐴) → ((𝐽 ↾t 𝐴) fLim 𝑎) = ((𝐽 ↾t 𝐴) fLim (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))) |
27 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑎 = (((nei‘𝐽)‘{𝑋}) ↾t 𝐴) → (𝐾 fLimf 𝑎) = (𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))) |
28 | 27 | fveq1d 6193 |
. . . . . . 7
⊢ (𝑎 = (((nei‘𝐽)‘{𝑋}) ↾t 𝐴) → ((𝐾 fLimf 𝑎)‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)) |
29 | 28 | eleq2d 2687 |
. . . . . 6
⊢ (𝑎 = (((nei‘𝐽)‘{𝑋}) ↾t 𝐴) → ((𝐹‘𝑥) ∈ ((𝐾 fLimf 𝑎)‘𝐹) ↔ (𝐹‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))) |
30 | 26, 29 | raleqbidv 3152 |
. . . . 5
⊢ (𝑎 = (((nei‘𝐽)‘{𝑋}) ↾t 𝐴) → (∀𝑥 ∈ ((𝐽 ↾t 𝐴) fLim 𝑎)(𝐹‘𝑥) ∈ ((𝐾 fLimf 𝑎)‘𝐹) ↔ ∀𝑥 ∈ ((𝐽 ↾t 𝐴) fLim (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))(𝐹‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))) |
31 | 30 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 = (((nei‘𝐽)‘{𝑋}) ↾t 𝐴)) → (∀𝑥 ∈ ((𝐽 ↾t 𝐴) fLim 𝑎)(𝐹‘𝑥) ∈ ((𝐾 fLimf 𝑎)‘𝐹) ↔ ∀𝑥 ∈ ((𝐽 ↾t 𝐴) fLim (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))(𝐹‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))) |
32 | 25, 31 | rspcdv 3312 |
. . 3
⊢ (𝜑 → (∀𝑎 ∈ (Fil‘𝐴)∀𝑥 ∈ ((𝐽 ↾t 𝐴) fLim 𝑎)(𝐹‘𝑥) ∈ ((𝐾 fLimf 𝑎)‘𝐹) → ∀𝑥 ∈ ((𝐽 ↾t 𝐴) fLim (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))(𝐹‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))) |
33 | 17, 32 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ((𝐽 ↾t 𝐴) fLim (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))(𝐹‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)) |
34 | | neiflim 21778 |
. . . . 5
⊢ (((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ ((𝐽 ↾t 𝐴) fLim ((nei‘(𝐽 ↾t 𝐴))‘{𝑋}))) |
35 | 8, 20, 34 | syl2anc 693 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ((𝐽 ↾t 𝐴) fLim ((nei‘(𝐽 ↾t 𝐴))‘{𝑋}))) |
36 | 20 | snssd 4340 |
. . . . . 6
⊢ (𝜑 → {𝑋} ⊆ 𝐴) |
37 | 3 | neitr 20984 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶 ∧ {𝑋} ⊆ 𝐴) → ((nei‘(𝐽 ↾t 𝐴))‘{𝑋}) = (((nei‘𝐽)‘{𝑋}) ↾t 𝐴)) |
38 | 2, 6, 36, 37 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → ((nei‘(𝐽 ↾t 𝐴))‘{𝑋}) = (((nei‘𝐽)‘{𝑋}) ↾t 𝐴)) |
39 | 38 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → ((𝐽 ↾t 𝐴) fLim ((nei‘(𝐽 ↾t 𝐴))‘{𝑋})) = ((𝐽 ↾t 𝐴) fLim (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))) |
40 | 35, 39 | eleqtrd 2703 |
. . 3
⊢ (𝜑 → 𝑋 ∈ ((𝐽 ↾t 𝐴) fLim (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))) |
41 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
42 | 41 | eleq1d 2686 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ↔ (𝐹‘𝑋) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))) |
43 | 42 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((𝐹‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) ↔ (𝐹‘𝑋) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))) |
44 | 40, 43 | rspcdv 3312 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ ((𝐽 ↾t 𝐴) fLim (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))(𝐹‘𝑥) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹) → (𝐹‘𝑋) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))) |
45 | 33, 44 | mpd 15 |
1
⊢ (𝜑 → (𝐹‘𝑋) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)) |