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 22139 |
. . . 4
⊢ (𝐸 ∈ (Met‘𝑉) → 𝐸 ∈ (∞Met‘𝑉)) |
11 | 9, 10 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 11 | prdsxmet 22174 |
. 2
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵)) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 11 | prdsdsf 22172 |
. . . 4
⊢ (𝜑 → 𝐷:(𝐵 × 𝐵)⟶(0[,]+∞)) |
14 | | ffn 6045 |
. . . 4
⊢ (𝐷:(𝐵 × 𝐵)⟶(0[,]+∞) → 𝐷 Fn (𝐵 × 𝐵)) |
15 | 13, 14 | syl 17 |
. . 3
⊢ (𝜑 → 𝐷 Fn (𝐵 × 𝐵)) |
16 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑆 ∈ 𝑊) |
17 | 7 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐼 ∈ Fin) |
18 | 8 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑍) |
19 | 18 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑍) |
20 | | simprl 794 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ 𝐵) |
21 | | simprr 796 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ 𝐵) |
22 | 1, 2, 16, 17, 19, 20, 21, 3, 4, 5 | prdsdsval3 16145 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, <
)) |
23 | 1, 2, 16, 17, 19, 3, 20 | prdsbascl 16143 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ 𝑉) |
24 | 1, 2, 16, 17, 19, 3, 21 | prdsbascl 16143 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉) |
25 | | r19.26 3064 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐼 ((𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) ↔ (∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉)) |
26 | | metcl 22137 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸 ∈ (Met‘𝑉) ∧ (𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ) |
27 | 26 | 3expib 1268 |
. . . . . . . . . . . . . 14
⊢ (𝐸 ∈ (Met‘𝑉) → (((𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ)) |
28 | 9, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (((𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) → ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ)) |
29 | 28 | ralimdva 2962 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) → ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ)) |
30 | 29 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (∀𝑥 ∈ 𝐼 ((𝑓‘𝑥) ∈ 𝑉 ∧ (𝑔‘𝑥) ∈ 𝑉) → ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ)) |
31 | 25, 30 | syl5bir 233 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ((∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉) → ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ)) |
32 | 23, 24, 31 | mp2and 715 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ) |
33 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) |
34 | 33 | fmpt 6381 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐼 ((𝑓‘𝑥)𝐸(𝑔‘𝑥)) ∈ ℝ ↔ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))):𝐼⟶ℝ) |
35 | 32, 34 | sylib 208 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))):𝐼⟶ℝ) |
36 | | frn 6053 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))):𝐼⟶ℝ → ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ⊆ ℝ) |
37 | 35, 36 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ⊆ ℝ) |
38 | | 0red 10041 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 0 ∈ ℝ) |
39 | 38 | snssd 4340 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → {0} ⊆
ℝ) |
40 | 37, 39 | unssd 3789 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ⊆
ℝ) |
41 | | xrltso 11974 |
. . . . . . . 8
⊢ < Or
ℝ* |
42 | 41 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → < Or
ℝ*) |
43 | | mptfi 8265 |
. . . . . . . . 9
⊢ (𝐼 ∈ Fin → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∈ Fin) |
44 | | rnfi 8249 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∈ Fin → ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∈ Fin) |
45 | 17, 43, 44 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∈ Fin) |
46 | | snfi 8038 |
. . . . . . . 8
⊢ {0}
∈ Fin |
47 | | unfi 8227 |
. . . . . . . 8
⊢ ((ran
(𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∈ Fin ∧ {0} ∈ Fin) →
(ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ∈ Fin) |
48 | 45, 46, 47 | sylancl 694 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ∈ Fin) |
49 | | ssun2 3777 |
. . . . . . . . 9
⊢ {0}
⊆ (ran (𝑥 ∈
𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) |
50 | | c0ex 10034 |
. . . . . . . . . 10
⊢ 0 ∈
V |
51 | 50 | snss 4316 |
. . . . . . . . 9
⊢ (0 ∈
(ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ↔ {0} ⊆ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0})) |
52 | 49, 51 | mpbir 221 |
. . . . . . . 8
⊢ 0 ∈
(ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) |
53 | | ne0i 3921 |
. . . . . . . 8
⊢ (0 ∈
(ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ≠ ∅) |
54 | 52, 53 | mp1i 13 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ≠ ∅) |
55 | | ressxr 10083 |
. . . . . . . 8
⊢ ℝ
⊆ ℝ* |
56 | 40, 55 | syl6ss 3615 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ⊆
ℝ*) |
57 | | fisupcl 8375 |
. . . . . . 7
⊢ (( <
Or ℝ* ∧ ((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ∈ Fin ∧ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ≠ ∅ ∧ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}) ⊆ ℝ*))
→ sup((ran (𝑥 ∈
𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, < )
∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0})) |
58 | 42, 48, 54, 56, 57 | syl13anc 1328 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, < )
∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0})) |
59 | 40, 58 | sseldd 3604 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)𝐸(𝑔‘𝑥))) ∪ {0}), ℝ*, < )
∈ ℝ) |
60 | 22, 59 | eqeltrd 2701 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑓𝐷𝑔) ∈ ℝ) |
61 | 60 | ralrimivva 2971 |
. . 3
⊢ (𝜑 → ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑓𝐷𝑔) ∈ ℝ) |
62 | | ffnov 6764 |
. . 3
⊢ (𝐷:(𝐵 × 𝐵)⟶ℝ ↔ (𝐷 Fn (𝐵 × 𝐵) ∧ ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑓𝐷𝑔) ∈ ℝ)) |
63 | 15, 61, 62 | sylanbrc 698 |
. 2
⊢ (𝜑 → 𝐷:(𝐵 × 𝐵)⟶ℝ) |
64 | | ismet2 22138 |
. 2
⊢ (𝐷 ∈ (Met‘𝐵) ↔ (𝐷 ∈ (∞Met‘𝐵) ∧ 𝐷:(𝐵 × 𝐵)⟶ℝ)) |
65 | 12, 63, 64 | sylanbrc 698 |
1
⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) |