Step | Hyp | Ref
| Expression |
1 | | elfvex 6221 |
. 2
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝑋 ∈ V) |
2 | | elfvex 6221 |
. . 3
⊢ (𝐷 ∈ (Met‘𝑋) → 𝑋 ∈ V) |
3 | 2 | adantr 481 |
. 2
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ∀𝑓 ∈ (CauFil‘𝐷)(𝐽 fLim 𝑓) ≠ ∅) → 𝑋 ∈ V) |
4 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (Met‘𝑥) = (Met‘𝑋)) |
5 | | rabeq 3192 |
. . . . . 6
⊢
((Met‘𝑥) =
(Met‘𝑋) → {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅} = {𝑑 ∈ (Met‘𝑋) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (𝑥 = 𝑋 → {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅} = {𝑑 ∈ (Met‘𝑋) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}) |
7 | | df-cmet 23055 |
. . . . 5
⊢ CMet =
(𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}) |
8 | | fvex 6201 |
. . . . . 6
⊢
(Met‘𝑋) ∈
V |
9 | 8 | rabex 4813 |
. . . . 5
⊢ {𝑑 ∈ (Met‘𝑋) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅} ∈ V |
10 | 6, 7, 9 | fvmpt 6282 |
. . . 4
⊢ (𝑋 ∈ V →
(CMet‘𝑋) = {𝑑 ∈ (Met‘𝑋) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}) |
11 | 10 | eleq2d 2687 |
. . 3
⊢ (𝑋 ∈ V → (𝐷 ∈ (CMet‘𝑋) ↔ 𝐷 ∈ {𝑑 ∈ (Met‘𝑋) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})) |
12 | | fveq2 6191 |
. . . . 5
⊢ (𝑑 = 𝐷 → (CauFil‘𝑑) = (CauFil‘𝐷)) |
13 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (MetOpen‘𝑑) = (MetOpen‘𝐷)) |
14 | | iscmet.1 |
. . . . . . . 8
⊢ 𝐽 = (MetOpen‘𝐷) |
15 | 13, 14 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → (MetOpen‘𝑑) = 𝐽) |
16 | 15 | oveq1d 6665 |
. . . . . 6
⊢ (𝑑 = 𝐷 → ((MetOpen‘𝑑) fLim 𝑓) = (𝐽 fLim 𝑓)) |
17 | 16 | neeq1d 2853 |
. . . . 5
⊢ (𝑑 = 𝐷 → (((MetOpen‘𝑑) fLim 𝑓) ≠ ∅ ↔ (𝐽 fLim 𝑓) ≠ ∅)) |
18 | 12, 17 | raleqbidv 3152 |
. . . 4
⊢ (𝑑 = 𝐷 → (∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅ ↔ ∀𝑓 ∈ (CauFil‘𝐷)(𝐽 fLim 𝑓) ≠ ∅)) |
19 | 18 | elrab 3363 |
. . 3
⊢ (𝐷 ∈ {𝑑 ∈ (Met‘𝑋) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅} ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑓 ∈ (CauFil‘𝐷)(𝐽 fLim 𝑓) ≠ ∅)) |
20 | 11, 19 | syl6bb 276 |
. 2
⊢ (𝑋 ∈ V → (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑓 ∈ (CauFil‘𝐷)(𝐽 fLim 𝑓) ≠ ∅))) |
21 | 1, 3, 20 | pm5.21nii 368 |
1
⊢ (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑓 ∈ (CauFil‘𝐷)(𝐽 fLim 𝑓) ≠ ∅)) |