Step | Hyp | Ref
| Expression |
1 | | df-metu 20141 |
. . 3
⊢ metUnif =
(𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))))) |
2 | 1 | a1i 11 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → metUnif = (𝑑 ∈ ∪ ran PsMet ↦ ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))))) |
3 | | simpr 479 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷) |
4 | 3 | dmeqd 5571 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom 𝑑 = dom 𝐷) |
5 | 4 | dmeqd 5571 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = dom dom 𝐷) |
6 | | psmetdmdm 22518 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) |
7 | 6 | adantr 474 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑋 = dom dom 𝐷) |
8 | 5, 7 | eqtr4d 2816 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = 𝑋) |
9 | 8 | sqxpeqd 5387 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (dom dom 𝑑 × dom dom 𝑑) = (𝑋 × 𝑋)) |
10 | | simplr 759 |
. . . . . . 7
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) ∧ 𝑎 ∈ ℝ+) → 𝑑 = 𝐷) |
11 | 10 | cnveqd 5543 |
. . . . . 6
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) ∧ 𝑎 ∈ ℝ+) → ◡𝑑 = ◡𝐷) |
12 | 11 | imaeq1d 5719 |
. . . . 5
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) ∧ 𝑎 ∈ ℝ+) → (◡𝑑 “ (0[,)𝑎)) = (◡𝐷 “ (0[,)𝑎))) |
13 | 12 | mpteq2dva 4979 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))) = (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))) |
14 | 13 | rneqd 5598 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))) = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))) |
15 | 9, 14 | oveq12d 6940 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))))) |
16 | | elfvdm 6478 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ dom PsMet) |
17 | | fveq2 6446 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (PsMet‘𝑥) = (PsMet‘𝑋)) |
18 | 17 | eleq2d 2844 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐷 ∈ (PsMet‘𝑥) ↔ 𝐷 ∈ (PsMet‘𝑋))) |
19 | 18 | rspcev 3510 |
. . . 4
⊢ ((𝑋 ∈ dom PsMet ∧ 𝐷 ∈ (PsMet‘𝑋)) → ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥)) |
20 | 16, 19 | mpancom 678 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥)) |
21 | | df-psmet 20134 |
. . . . 5
⊢ PsMet =
(𝑦 ∈ V ↦ {𝑢 ∈ (ℝ*
↑𝑚 (𝑦 × 𝑦)) ∣ ∀𝑧 ∈ 𝑦 ((𝑧𝑢𝑧) = 0 ∧ ∀𝑤 ∈ 𝑦 ∀𝑣 ∈ 𝑦 (𝑧𝑢𝑤) ≤ ((𝑣𝑢𝑧) +𝑒 (𝑣𝑢𝑤)))}) |
22 | 21 | funmpt2 6174 |
. . . 4
⊢ Fun
PsMet |
23 | | elunirn 6781 |
. . . 4
⊢ (Fun
PsMet → (𝐷 ∈
∪ ran PsMet ↔ ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥))) |
24 | 22, 23 | ax-mp 5 |
. . 3
⊢ (𝐷 ∈ ∪ ran PsMet ↔ ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥)) |
25 | 20, 24 | sylibr 226 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷 ∈ ∪ ran
PsMet) |
26 | | ovexd 6956 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))) ∈ V) |
27 | 2, 15, 25, 26 | fvmptd 6548 |
1
⊢ (𝐷 ∈ (PsMet‘𝑋) → (metUnif‘𝐷) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))))) |