Proof of Theorem cnextucn
Step | Hyp | Ref
| Expression |
1 | | eqid 2825 |
. 2
⊢ ∪ 𝐽 =
∪ 𝐽 |
2 | | eqid 2825 |
. 2
⊢ ∪ 𝐾 =
∪ 𝐾 |
3 | | cnextucn.v |
. . 3
⊢ (𝜑 → 𝑉 ∈ TopSp) |
4 | | cnextucn.j |
. . . 4
⊢ 𝐽 = (TopOpen‘𝑉) |
5 | 4 | tpstop 21112 |
. . 3
⊢ (𝑉 ∈ TopSp → 𝐽 ∈ Top) |
6 | 3, 5 | syl 17 |
. 2
⊢ (𝜑 → 𝐽 ∈ Top) |
7 | | cnextucn.h |
. 2
⊢ (𝜑 → 𝐾 ∈ Haus) |
8 | | cnextucn.f |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝑌) |
9 | | cnextucn.t |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ TopSp) |
10 | | cnextucn.y |
. . . . . 6
⊢ 𝑌 = (Base‘𝑊) |
11 | | cnextucn.k |
. . . . . 6
⊢ 𝐾 = (TopOpen‘𝑊) |
12 | 10, 11 | tpsuni 21111 |
. . . . 5
⊢ (𝑊 ∈ TopSp → 𝑌 = ∪
𝐾) |
13 | 9, 12 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑌 = ∪ 𝐾) |
14 | 13 | feq3d 6265 |
. . 3
⊢ (𝜑 → (𝐹:𝐴⟶𝑌 ↔ 𝐹:𝐴⟶∪ 𝐾)) |
15 | 8, 14 | mpbid 224 |
. 2
⊢ (𝜑 → 𝐹:𝐴⟶∪ 𝐾) |
16 | | cnextucn.a |
. . 3
⊢ (𝜑 → 𝐴 ⊆ 𝑋) |
17 | | cnextucn.x |
. . . . 5
⊢ 𝑋 = (Base‘𝑉) |
18 | 17, 4 | tpsuni 21111 |
. . . 4
⊢ (𝑉 ∈ TopSp → 𝑋 = ∪
𝐽) |
19 | 3, 18 | syl 17 |
. . 3
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
20 | 16, 19 | sseqtrd 3866 |
. 2
⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐽) |
21 | | cnextucn.c |
. . 3
⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋) |
22 | 21, 19 | eqtrd 2861 |
. 2
⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = ∪ 𝐽) |
23 | 10, 11 | istps 21109 |
. . . . . 6
⊢ (𝑊 ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑌)) |
24 | 9, 23 | sylib 210 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
25 | 24 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → 𝐾 ∈ (TopOn‘𝑌)) |
26 | 19 | eleq2d 2892 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝐽)) |
27 | 26 | biimpar 471 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → 𝑥 ∈ 𝑋) |
28 | 21 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → ((cls‘𝐽)‘𝐴) = 𝑋) |
29 | 27, 28 | eleqtrrd 2909 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → 𝑥 ∈ ((cls‘𝐽)‘𝐴)) |
30 | 1 | toptopon 21092 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
31 | 6, 30 | sylib 210 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
32 | | fveq2 6433 |
. . . . . . . . . 10
⊢ (𝑋 = ∪
𝐽 → (TopOn‘𝑋) = (TopOn‘∪ 𝐽)) |
33 | 32 | eleq2d 2892 |
. . . . . . . . 9
⊢ (𝑋 = ∪
𝐽 → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))) |
34 | 19, 33 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))) |
35 | 31, 34 | mpbird 249 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
36 | 35 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → 𝐽 ∈ (TopOn‘𝑋)) |
37 | 16 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → 𝐴 ⊆ 𝑋) |
38 | | trnei 22066 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴))) |
39 | 36, 37, 27, 38 | syl3anc 1496 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴))) |
40 | 29, 39 | mpbid 224 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴)) |
41 | 8 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → 𝐹:𝐴⟶𝑌) |
42 | | flfval 22164 |
. . . 4
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝑌) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴)))) |
43 | 25, 40, 41, 42 | syl3anc 1496 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = (𝐾 fLim ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴)))) |
44 | | cnextucn.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ CUnifSp) |
45 | 44 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → 𝑊 ∈ CUnifSp) |
46 | | cnextucn.l |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∈ (CauFilu‘𝑈)) |
47 | 27, 46 | syldan 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∈ (CauFilu‘𝑈)) |
48 | | cnextucn.u |
. . . . . 6
⊢ 𝑈 = (UnifSt‘𝑊) |
49 | 48 | fveq2i 6436 |
. . . . 5
⊢
(CauFilu‘𝑈) =
(CauFilu‘(UnifSt‘𝑊)) |
50 | 47, 49 | syl6eleq 2916 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∈
(CauFilu‘(UnifSt‘𝑊))) |
51 | 10 | fvexi 6447 |
. . . . . 6
⊢ 𝑌 ∈ V |
52 | 51 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → 𝑌 ∈ V) |
53 | | filfbas 22022 |
. . . . . 6
⊢
((((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (Fil‘𝐴) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (fBas‘𝐴)) |
54 | 40, 53 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (fBas‘𝐴)) |
55 | | fmfil 22118 |
. . . . 5
⊢ ((𝑌 ∈ V ∧
(((nei‘𝐽)‘{𝑥}) ↾t 𝐴) ∈ (fBas‘𝐴) ∧ 𝐹:𝐴⟶𝑌) → ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∈ (Fil‘𝑌)) |
56 | 52, 54, 41, 55 | syl3anc 1496 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∈ (Fil‘𝑌)) |
57 | 10, 11 | cuspcvg 22475 |
. . . 4
⊢ ((𝑊 ∈ CUnifSp ∧ ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∈
(CauFilu‘(UnifSt‘𝑊)) ∧ ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) ∈ (Fil‘𝑌)) → (𝐾 fLim ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴))) ≠ ∅) |
58 | 45, 50, 56, 57 | syl3anc 1496 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → (𝐾 fLim ((𝑌 FilMap 𝐹)‘(((nei‘𝐽)‘{𝑥}) ↾t 𝐴))) ≠ ∅) |
59 | 43, 58 | eqnetrd 3066 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝐽) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) |
60 | | cuspusp 22474 |
. . . 4
⊢ (𝑊 ∈ CUnifSp → 𝑊 ∈ UnifSp) |
61 | 44, 60 | syl 17 |
. . 3
⊢ (𝜑 → 𝑊 ∈ UnifSp) |
62 | 11 | uspreg 22448 |
. . 3
⊢ ((𝑊 ∈ UnifSp ∧ 𝐾 ∈ Haus) → 𝐾 ∈ Reg) |
63 | 61, 7, 62 | syl2anc 581 |
. 2
⊢ (𝜑 → 𝐾 ∈ Reg) |
64 | 1, 2, 6, 7, 15, 20, 22, 59, 63 | cnextcn 22241 |
1
⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾)) |