Step | Hyp | Ref
| Expression |
1 | | df-metu 20577 |
. 2
⊢ metUnif =
(𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))))) |
2 | | simpr 484 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷) |
3 | 2 | dmeqd 5811 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom 𝑑 = dom 𝐷) |
4 | 3 | dmeqd 5811 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = dom dom 𝐷) |
5 | | psmetdmdm 23439 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) |
6 | 5 | adantr 480 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑋 = dom dom 𝐷) |
7 | 4, 6 | eqtr4d 2782 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = 𝑋) |
8 | 7 | sqxpeqd 5620 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (dom dom 𝑑 × dom dom 𝑑) = (𝑋 × 𝑋)) |
9 | | simplr 765 |
. . . . . . 7
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) ∧ 𝑎 ∈ ℝ+) → 𝑑 = 𝐷) |
10 | 9 | cnveqd 5781 |
. . . . . 6
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) ∧ 𝑎 ∈ ℝ+) → ◡𝑑 = ◡𝐷) |
11 | 10 | imaeq1d 5965 |
. . . . 5
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) ∧ 𝑎 ∈ ℝ+) → (◡𝑑 “ (0[,)𝑎)) = (◡𝐷 “ (0[,)𝑎))) |
12 | 11 | mpteq2dva 5178 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))) = (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))) |
13 | 12 | rneqd 5844 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))) = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))) |
14 | 8, 13 | oveq12d 7286 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))))) |
15 | | elfvdm 6800 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ dom PsMet) |
16 | | fveq2 6768 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (PsMet‘𝑥) = (PsMet‘𝑋)) |
17 | 16 | eleq2d 2825 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐷 ∈ (PsMet‘𝑥) ↔ 𝐷 ∈ (PsMet‘𝑋))) |
18 | 17 | rspcev 3560 |
. . . 4
⊢ ((𝑋 ∈ dom PsMet ∧ 𝐷 ∈ (PsMet‘𝑋)) → ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥)) |
19 | 15, 18 | mpancom 684 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥)) |
20 | | df-psmet 20570 |
. . . . 5
⊢ PsMet =
(𝑦 ∈ V ↦ {𝑢 ∈ (ℝ*
↑m (𝑦
× 𝑦)) ∣
∀𝑧 ∈ 𝑦 ((𝑧𝑢𝑧) = 0 ∧ ∀𝑤 ∈ 𝑦 ∀𝑣 ∈ 𝑦 (𝑧𝑢𝑤) ≤ ((𝑣𝑢𝑧) +𝑒 (𝑣𝑢𝑤)))}) |
21 | 20 | funmpt2 6469 |
. . . 4
⊢ Fun
PsMet |
22 | | elunirn 7118 |
. . . 4
⊢ (Fun
PsMet → (𝐷 ∈
∪ ran PsMet ↔ ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥))) |
23 | 21, 22 | ax-mp 5 |
. . 3
⊢ (𝐷 ∈ ∪ ran PsMet ↔ ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥)) |
24 | 19, 23 | sylibr 233 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷 ∈ ∪ ran
PsMet) |
25 | | ovexd 7303 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))) ∈ V) |
26 | 1, 14, 24, 25 | fvmptd2 6877 |
1
⊢ (𝐷 ∈ (PsMet‘𝑋) → (metUnif‘𝐷) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))))) |