Step | Hyp | Ref
| Expression |
1 | | cmetmet 23604 |
. . 3
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
2 | | metsscmetcld.j |
. . . 4
⊢ 𝐽 = (MetOpen‘𝐷) |
3 | 2 | metsscmetcld 23633 |
. . 3
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌)) → 𝑌 ∈ (Clsd‘𝐽)) |
4 | 1, 3 | sylan 572 |
. 2
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌)) → 𝑌 ∈ (Clsd‘𝐽)) |
5 | 1 | adantr 473 |
. . . 4
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) → 𝐷 ∈ (Met‘𝑋)) |
6 | | eqid 2772 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
7 | 6 | cldss 21353 |
. . . . . 6
⊢ (𝑌 ∈ (Clsd‘𝐽) → 𝑌 ⊆ ∪ 𝐽) |
8 | 7 | adantl 474 |
. . . . 5
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) → 𝑌 ⊆ ∪ 𝐽) |
9 | | metxmet 22659 |
. . . . . 6
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
10 | 2 | mopnuni 22766 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
11 | 5, 9, 10 | 3syl 18 |
. . . . 5
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) → 𝑋 = ∪ 𝐽) |
12 | 8, 11 | sseqtr4d 3892 |
. . . 4
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) → 𝑌 ⊆ 𝑋) |
13 | | metres2 22688 |
. . . 4
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (Met‘𝑌)) |
14 | 5, 12, 13 | syl2anc 576 |
. . 3
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (Met‘𝑌)) |
15 | 1, 9 | syl 17 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
16 | 15 | ad2antrr 713 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝐷 ∈ (∞Met‘𝑋)) |
17 | 12 | adantr 473 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝑌 ⊆ 𝑋) |
18 | | eqid 2772 |
. . . . . . . . . 10
⊢ (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌)) |
19 | | eqid 2772 |
. . . . . . . . . 10
⊢
(MetOpen‘(𝐷
↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) |
20 | 18, 2, 19 | metrest 22849 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))) |
21 | 16, 17, 20 | syl2anc 576 |
. . . . . . . 8
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → (𝐽 ↾t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))) |
22 | 21 | eqcomd 2778 |
. . . . . . 7
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (𝐽 ↾t 𝑌)) |
23 | | metxmet 22659 |
. . . . . . . . . . 11
⊢ ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (Met‘𝑌) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) |
24 | 14, 23 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) |
25 | | cfilfil 23585 |
. . . . . . . . . 10
⊢ (((𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝑓 ∈ (Fil‘𝑌)) |
26 | 24, 25 | sylan 572 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝑓 ∈ (Fil‘𝑌)) |
27 | | elfvdm 6528 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝑋 ∈ dom CMet) |
28 | 27 | ad2antrr 713 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝑋 ∈ dom CMet) |
29 | | trfg 22215 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (Fil‘𝑌) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ dom CMet) → ((𝑋filGen𝑓) ↾t 𝑌) = 𝑓) |
30 | 26, 17, 28, 29 | syl3anc 1351 |
. . . . . . . 8
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((𝑋filGen𝑓) ↾t 𝑌) = 𝑓) |
31 | 30 | eqcomd 2778 |
. . . . . . 7
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝑓 = ((𝑋filGen𝑓) ↾t 𝑌)) |
32 | 22, 31 | oveq12d 6992 |
. . . . . 6
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim 𝑓) = ((𝐽 ↾t 𝑌) fLim ((𝑋filGen𝑓) ↾t 𝑌))) |
33 | 2 | mopntopon 22764 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
34 | 16, 33 | syl 17 |
. . . . . . 7
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝐽 ∈ (TopOn‘𝑋)) |
35 | | filfbas 22172 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (Fil‘𝑌) → 𝑓 ∈ (fBas‘𝑌)) |
36 | 26, 35 | syl 17 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝑓 ∈ (fBas‘𝑌)) |
37 | | filsspw 22175 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (Fil‘𝑌) → 𝑓 ⊆ 𝒫 𝑌) |
38 | 26, 37 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝑓 ⊆ 𝒫 𝑌) |
39 | | sspwb 5194 |
. . . . . . . . . . 11
⊢ (𝑌 ⊆ 𝑋 ↔ 𝒫 𝑌 ⊆ 𝒫 𝑋) |
40 | 17, 39 | sylib 210 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝒫 𝑌 ⊆ 𝒫 𝑋) |
41 | 38, 40 | sstrd 3862 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝑓 ⊆ 𝒫 𝑋) |
42 | | fbasweak 22189 |
. . . . . . . . 9
⊢ ((𝑓 ∈ (fBas‘𝑌) ∧ 𝑓 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ dom CMet) → 𝑓 ∈ (fBas‘𝑋)) |
43 | 36, 41, 28, 42 | syl3anc 1351 |
. . . . . . . 8
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝑓 ∈ (fBas‘𝑋)) |
44 | | fgcl 22202 |
. . . . . . . 8
⊢ (𝑓 ∈ (fBas‘𝑋) → (𝑋filGen𝑓) ∈ (Fil‘𝑋)) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → (𝑋filGen𝑓) ∈ (Fil‘𝑋)) |
46 | | ssfg 22196 |
. . . . . . . . 9
⊢ (𝑓 ∈ (fBas‘𝑋) → 𝑓 ⊆ (𝑋filGen𝑓)) |
47 | 43, 46 | syl 17 |
. . . . . . . 8
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝑓 ⊆ (𝑋filGen𝑓)) |
48 | | filtop 22179 |
. . . . . . . . 9
⊢ (𝑓 ∈ (Fil‘𝑌) → 𝑌 ∈ 𝑓) |
49 | 26, 48 | syl 17 |
. . . . . . . 8
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝑌 ∈ 𝑓) |
50 | 47, 49 | sseldd 3853 |
. . . . . . 7
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝑌 ∈ (𝑋filGen𝑓)) |
51 | | flimrest 22307 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen𝑓) ∈ (Fil‘𝑋) ∧ 𝑌 ∈ (𝑋filGen𝑓)) → ((𝐽 ↾t 𝑌) fLim ((𝑋filGen𝑓) ↾t 𝑌)) = ((𝐽 fLim (𝑋filGen𝑓)) ∩ 𝑌)) |
52 | 34, 45, 50, 51 | syl3anc 1351 |
. . . . . 6
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((𝐽 ↾t 𝑌) fLim ((𝑋filGen𝑓) ↾t 𝑌)) = ((𝐽 fLim (𝑋filGen𝑓)) ∩ 𝑌)) |
53 | | flimclsi 22302 |
. . . . . . . . 9
⊢ (𝑌 ∈ (𝑋filGen𝑓) → (𝐽 fLim (𝑋filGen𝑓)) ⊆ ((cls‘𝐽)‘𝑌)) |
54 | 50, 53 | syl 17 |
. . . . . . . 8
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → (𝐽 fLim (𝑋filGen𝑓)) ⊆ ((cls‘𝐽)‘𝑌)) |
55 | | cldcls 21366 |
. . . . . . . . 9
⊢ (𝑌 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑌) = 𝑌) |
56 | 55 | ad2antlr 714 |
. . . . . . . 8
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((cls‘𝐽)‘𝑌) = 𝑌) |
57 | 54, 56 | sseqtrd 3891 |
. . . . . . 7
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → (𝐽 fLim (𝑋filGen𝑓)) ⊆ 𝑌) |
58 | | df-ss 3837 |
. . . . . . 7
⊢ ((𝐽 fLim (𝑋filGen𝑓)) ⊆ 𝑌 ↔ ((𝐽 fLim (𝑋filGen𝑓)) ∩ 𝑌) = (𝐽 fLim (𝑋filGen𝑓))) |
59 | 57, 58 | sylib 210 |
. . . . . 6
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((𝐽 fLim (𝑋filGen𝑓)) ∩ 𝑌) = (𝐽 fLim (𝑋filGen𝑓))) |
60 | 32, 52, 59 | 3eqtrd 2812 |
. . . . 5
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim 𝑓) = (𝐽 fLim (𝑋filGen𝑓))) |
61 | | simpll 754 |
. . . . . 6
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → 𝐷 ∈ (CMet‘𝑋)) |
62 | 5, 9 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) → 𝐷 ∈ (∞Met‘𝑋)) |
63 | | cfilresi 23613 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → (𝑋filGen𝑓) ∈ (CauFil‘𝐷)) |
64 | 62, 63 | sylan 572 |
. . . . . 6
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → (𝑋filGen𝑓) ∈ (CauFil‘𝐷)) |
65 | 2 | cmetcvg 23603 |
. . . . . 6
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑋filGen𝑓) ∈ (CauFil‘𝐷)) → (𝐽 fLim (𝑋filGen𝑓)) ≠ ∅) |
66 | 61, 64, 65 | syl2anc 576 |
. . . . 5
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → (𝐽 fLim (𝑋filGen𝑓)) ≠ ∅) |
67 | 60, 66 | eqnetrd 3028 |
. . . 4
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) ∧ 𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim 𝑓) ≠ ∅) |
68 | 67 | ralrimiva 3126 |
. . 3
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) → ∀𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim 𝑓) ≠ ∅) |
69 | 19 | iscmet 23602 |
. . 3
⊢ ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌) ↔ ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (Met‘𝑌) ∧ ∀𝑓 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim 𝑓) ≠ ∅)) |
70 | 14, 68, 69 | sylanbrc 575 |
. 2
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑌 ∈ (Clsd‘𝐽)) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌)) |
71 | 4, 70 | impbida 788 |
1
⊢ (𝐷 ∈ (CMet‘𝑋) → ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌) ↔ 𝑌 ∈ (Clsd‘𝐽))) |