Step | Hyp | Ref
| Expression |
1 | | prdsmet.y |
. . 3
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) |
2 | | prdsmet.b |
. . 3
⊢ 𝐵 = (Base‘𝑌) |
3 | | prdsmet.v |
. . 3
⊢ 𝑉 = (Base‘𝑅) |
4 | | prdsmet.e |
. . 3
⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) |
5 | | prdsmet.d |
. . 3
⊢ 𝐷 = (dist‘𝑌) |
6 | | prdsmet.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
7 | | prdsmet.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ Fin) |
8 | | prdsmet.r |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍) |
9 | | prdsmet.m |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉)) |
10 | | metxmet 21949 |
. . . 4
⊢ (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉)) |
11 | 9, 10 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 11 | prdsxmet 21984 |
. 2
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵)) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 11 | prdsdsf 21982 |
. . . 4
⊢ (𝜑 → 𝐷:(𝐵 × 𝐵)⟶(0[,]+∞)) |
14 | | ffn 5958 |
. . . 4
⊢ (𝐷:(𝐵 × 𝐵)⟶(0[,]+∞) → 𝐷 Fn (𝐵 × 𝐵)) |
15 | 13, 14 | syl 17 |
. . 3
⊢ (𝜑 → 𝐷 Fn (𝐵 × 𝐵)) |
16 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑆 ∈ 𝑊) |
17 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐼 ∈ Fin) |
18 | 8 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑍) |
19 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑍) |
20 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ 𝐵) |
21 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ 𝐵) |
22 | 1, 2, 16, 17, 19, 20, 21, 3, 4, 5 | prdsdsval3 15968 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, <
)) |
23 | 1, 2, 16, 17, 19, 3, 20 | prdsbascl 15966 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ 𝑉) |
24 | 1, 2, 16, 17, 19, 3, 21 | prdsbascl 15966 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉) |
25 | | r19.26 3046 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐼 ((𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) ↔ (∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉)) |
26 | | metcl 21947 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸 ∈ (Met‘𝑉) ∧ (𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ) |
27 | 26 | 3expib 1260 |
. . . . . . . . . . . . . 14
⊢ (𝐸 ∈ (Met‘𝑉) → (((𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ)) |
28 | 9, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (((𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ)) |
29 | 28 | ralimdva 2945 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) → ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ)) |
30 | 29 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) → ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ)) |
31 | 25, 30 | syl5bir 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ((∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉) → ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ)) |
32 | 23, 24, 31 | mp2and 711 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ) |
33 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) |
34 | 33 | fmpt 6289 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ ↔ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))):𝐼⟶ℝ) |
35 | 32, 34 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))):𝐼⟶ℝ) |
36 | | frn 5966 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))):𝐼⟶ℝ → ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ⊆ ℝ) |
37 | 35, 36 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ⊆ ℝ) |
38 | | 0red 9920 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 0 ∈ ℝ) |
39 | 38 | snssd 4281 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → {0} ⊆
ℝ) |
40 | 37, 39 | unssd 3751 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ⊆
ℝ) |
41 | | xrltso 11850 |
. . . . . . . 8
⊢ < Or
ℝ* |
42 | 41 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → < Or
ℝ*) |
43 | | mptfi 8148 |
. . . . . . . . 9
⊢ (𝐼 ∈ Fin → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∈ Fin) |
44 | | rnfi 8132 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∈ Fin → ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∈ Fin) |
45 | 17, 43, 44 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∈ Fin) |
46 | | snfi 7923 |
. . . . . . . 8
⊢ {0}
∈ Fin |
47 | | unfi 8112 |
. . . . . . . 8
⊢ ((ran
(𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∈ Fin ∧ {0} ∈ Fin) →
(ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ∈ Fin) |
48 | 45, 46, 47 | sylancl 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ∈ Fin) |
49 | | ssun2 3739 |
. . . . . . . . 9
⊢ {0}
⊆ (ran (𝑥 ∈
𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) |
50 | | c0ex 9913 |
. . . . . . . . . 10
⊢ 0 ∈
V |
51 | 50 | snss 4259 |
. . . . . . . . 9
⊢ (0 ∈
(ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ↔ {0} ⊆ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0})) |
52 | 49, 51 | mpbir 220 |
. . . . . . . 8
⊢ 0 ∈
(ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) |
53 | | ne0i 3880 |
. . . . . . . 8
⊢ (0 ∈
(ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ≠ ∅) |
54 | 52, 53 | mp1i 13 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ≠ ∅) |
55 | | ressxr 9962 |
. . . . . . . 8
⊢ ℝ
⊆ ℝ* |
56 | 40, 55 | syl6ss 3580 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ⊆
ℝ*) |
57 | | fisupcl 8258 |
. . . . . . 7
⊢ (( <
Or ℝ* ∧ ((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ∈ Fin ∧ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ≠ ∅ ∧ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ⊆ ℝ*))
→ sup((ran (𝑥 ∈
𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, < )
∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0})) |
58 | 42, 48, 54, 56, 57 | syl13anc 1320 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, < )
∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0})) |
59 | 40, 58 | sseldd 3569 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, < )
∈ ℝ) |
60 | 22, 59 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓𝐷𝑔) ∈ ℝ) |
61 | 60 | ralrimivva 2954 |
. . 3
⊢ (𝜑 → ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑓𝐷𝑔) ∈ ℝ) |
62 | | ffnov 6662 |
. . 3
⊢ (𝐷:(𝐵 × 𝐵)⟶ℝ ↔ (𝐷 Fn (𝐵 × 𝐵) ∧ ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑓𝐷𝑔) ∈ ℝ)) |
63 | 15, 61, 62 | sylanbrc 695 |
. 2
⊢ (𝜑 → 𝐷:(𝐵 × 𝐵)⟶ℝ) |
64 | | ismet2 21948 |
. 2
⊢ (𝐷 ∈ (Met‘𝐵) ↔ (𝐷 ∈ (∞Met‘𝐵) ∧ 𝐷:(𝐵 × 𝐵)⟶ℝ)) |
65 | 12, 63, 64 | sylanbrc 695 |
1
⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) |