Step | Hyp | Ref
| Expression |
1 | | df-metu 19566 |
. . 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 476 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷) |
4 | 3 | dmeqd 5248 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom 𝑑 = dom 𝐷) |
5 | 4 | dmeqd 5248 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = dom dom 𝐷) |
6 | | psmetdmdm 21920 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) |
7 | 6 | adantr 480 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → 𝑋 = dom dom 𝐷) |
8 | 5, 7 | eqtr4d 2647 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = 𝑋) |
9 | 8 | sqxpeqd 5065 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (dom dom 𝑑 × dom dom 𝑑) = (𝑋 × 𝑋)) |
10 | | simplr 788 |
. . . . . . 7
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) ∧ 𝑎 ∈ ℝ+) → 𝑑 = 𝐷) |
11 | 10 | cnveqd 5220 |
. . . . . 6
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) ∧ 𝑎 ∈ ℝ+) → ◡𝑑 = ◡𝐷) |
12 | 11 | imaeq1d 5384 |
. . . . 5
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) ∧ 𝑎 ∈ ℝ+) → (◡𝑑 “ (0[,)𝑎)) = (◡𝐷 “ (0[,)𝑎))) |
13 | 12 | mpteq2dva 4672 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))) = (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))) |
14 | 13 | rneqd 5274 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎))) = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))) |
15 | 9, 14 | oveq12d 6567 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑑 = 𝐷) → ((dom dom 𝑑 × dom dom 𝑑)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝑑 “ (0[,)𝑎)))) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))))) |
16 | | elfvdm 6130 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ dom PsMet) |
17 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (PsMet‘𝑥) = (PsMet‘𝑋)) |
18 | 17 | eleq2d 2673 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐷 ∈ (PsMet‘𝑥) ↔ 𝐷 ∈ (PsMet‘𝑋))) |
19 | 18 | rspcev 3282 |
. . . 4
⊢ ((𝑋 ∈ dom PsMet ∧ 𝐷 ∈ (PsMet‘𝑋)) → ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥)) |
20 | 16, 19 | mpancom 700 |
. . 3
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥)) |
21 | | df-psmet 19559 |
. . . . 5
⊢ PsMet =
(𝑦 ∈ V ↦ {𝑢 ∈ (ℝ*
↑𝑚 (𝑦 × 𝑦)) ∣ ∀𝑧 ∈ 𝑦 ((𝑧𝑢𝑧) = 0 ∧ ∀𝑤 ∈ 𝑦 ∀𝑣 ∈ 𝑦 (𝑧𝑢𝑤) ≤ ((𝑣𝑢𝑧) +𝑒 (𝑣𝑢𝑤)))}) |
22 | 21 | funmpt2 5841 |
. . . 4
⊢ Fun
PsMet |
23 | | elunirn 6413 |
. . . 4
⊢ (Fun
PsMet → (𝐷 ∈
∪ ran PsMet ↔ ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥))) |
24 | 22, 23 | ax-mp 5 |
. . 3
⊢ (𝐷 ∈ ∪ ran PsMet ↔ ∃𝑥 ∈ dom PsMet𝐷 ∈ (PsMet‘𝑥)) |
25 | 20, 24 | sylibr 223 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷 ∈ ∪ ran
PsMet) |
26 | | ovex 6577 |
. . 3
⊢ ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))) ∈ V |
27 | 26 | a1i 11 |
. 2
⊢ (𝐷 ∈ (PsMet‘𝑋) → ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))) ∈ V) |
28 | 2, 15, 25, 27 | fvmptd 6197 |
1
⊢ (𝐷 ∈ (PsMet‘𝑋) → (metUnif‘𝐷) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))))) |