Step | Hyp | Ref
| Expression |
1 | | fvssunirn 6127 |
. . . 4
⊢
(∞Met‘𝑋)
⊆ ∪ ran ∞Met |
2 | 1 | sseli 3564 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ ∪ ran
∞Met) |
3 | | dmeq 5246 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷) |
4 | 3 | dmeqd 5248 |
. . . . . 6
⊢ (𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷) |
5 | 4 | fveq2d 6107 |
. . . . 5
⊢ (𝑑 = 𝐷 → (Fil‘dom dom 𝑑) = (Fil‘dom dom 𝐷)) |
6 | | imaeq1 5380 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (𝑑 “ (𝑦 × 𝑦)) = (𝐷 “ (𝑦 × 𝑦))) |
7 | 6 | sseq1d 3595 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → ((𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
8 | 7 | rexbidv 3034 |
. . . . . 6
⊢ (𝑑 = 𝐷 → (∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
9 | 8 | ralbidv 2969 |
. . . . 5
⊢ (𝑑 = 𝐷 → (∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))) |
10 | 5, 9 | rabeqbidv 3168 |
. . . 4
⊢ (𝑑 = 𝐷 → {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)} = {𝑓 ∈ (Fil‘dom dom 𝐷) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}) |
11 | | df-cfil 22861 |
. . . 4
⊢ CauFil =
(𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}) |
12 | | fvex 6113 |
. . . . 5
⊢
(Fil‘dom dom 𝐷) ∈ V |
13 | 12 | rabex 4740 |
. . . 4
⊢ {𝑓 ∈ (Fil‘dom dom 𝐷) ∣ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)} ∈ V |
14 | 10, 11, 13 | fvmpt 6191 |
. . 3
⊢ (𝐷 ∈ ∪ ran ∞Met → (CauFil‘𝐷) = {𝑓 ∈ (Fil‘dom dom 𝐷) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}) |
15 | 2, 14 | syl 17 |
. 2
⊢ (𝐷 ∈ (∞Met‘𝑋) → (CauFil‘𝐷) = {𝑓 ∈ (Fil‘dom dom 𝐷) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}) |
16 | | xmetdmdm 21950 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = dom dom 𝐷) |
17 | 16 | fveq2d 6107 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → (Fil‘𝑋) = (Fil‘dom dom 𝐷)) |
18 | | rabeq 3166 |
. . 3
⊢
((Fil‘𝑋) =
(Fil‘dom dom 𝐷)
→ {𝑓 ∈
(Fil‘𝑋) ∣
∀𝑥 ∈
ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)} = {𝑓 ∈ (Fil‘dom dom 𝐷) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}) |
19 | 17, 18 | syl 17 |
. 2
⊢ (𝐷 ∈ (∞Met‘𝑋) → {𝑓 ∈ (Fil‘𝑋) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)} = {𝑓 ∈ (Fil‘dom dom 𝐷) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}) |
20 | 15, 19 | eqtr4d 2647 |
1
⊢ (𝐷 ∈ (∞Met‘𝑋) → (CauFil‘𝐷) = {𝑓 ∈ (Fil‘𝑋) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}) |