Step | Hyp | Ref
| Expression |
1 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
2 | | prdsdsf.r |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍) |
3 | | elex 3344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ 𝑍 → 𝑅 ∈ V) |
4 | 2, 3 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ V) |
5 | 4 | ralrimiva 3096 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ V) |
6 | 5 | adantr 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 𝑅 ∈ V) |
7 | | nfcsb1v 3682 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑅 |
8 | 7 | nfel1 2909 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑅 ∈ V |
9 | | csbeq1a 3675 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → 𝑅 = ⦋𝑦 / 𝑥⦌𝑅) |
10 | 9 | eleq1d 2816 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑅 ∈ V ↔ ⦋𝑦 / 𝑥⦌𝑅 ∈ V)) |
11 | 8, 10 | rspc 3435 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐼 → (∀𝑥 ∈ 𝐼 𝑅 ∈ V → ⦋𝑦 / 𝑥⦌𝑅 ∈ V)) |
12 | 6, 11 | mpan9 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ⦋𝑦 / 𝑥⦌𝑅 ∈ V) |
13 | | eqid 2752 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐼 ↦ 𝑅) = (𝑥 ∈ 𝐼 ↦ 𝑅) |
14 | 13 | fvmpts 6439 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐼 ∧ ⦋𝑦 / 𝑥⦌𝑅 ∈ V) → ((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦) = ⦋𝑦 / 𝑥⦌𝑅) |
15 | 1, 12, 14 | syl2anc 696 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦) = ⦋𝑦 / 𝑥⦌𝑅) |
16 | 15 | fveq2d 6348 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → (dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦)) = (dist‘⦋𝑦 / 𝑥⦌𝑅)) |
17 | 16 | oveqd 6822 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦)) = ((𝑓‘𝑦)(dist‘⦋𝑦 / 𝑥⦌𝑅)(𝑔‘𝑦))) |
18 | | prdsdsf.y |
. . . . . . . . . . . . . 14
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) |
19 | | prdsdsf.b |
. . . . . . . . . . . . . 14
⊢ 𝐵 = (Base‘𝑌) |
20 | | prdsdsf.s |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
21 | 20 | adantr 472 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑆 ∈ 𝑊) |
22 | | prdsdsf.i |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐼 ∈ 𝑋) |
23 | 22 | adantr 472 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐼 ∈ 𝑋) |
24 | | prdsdsf.v |
. . . . . . . . . . . . . 14
⊢ 𝑉 = (Base‘𝑅) |
25 | | simprl 811 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ 𝐵) |
26 | 18, 19, 21, 23, 6, 24, 25 | prdsbascl 16337 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ 𝑉) |
27 | | nfcsb1v 3682 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑉 |
28 | 27 | nfel2 2911 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑓‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉 |
29 | | fveq2 6344 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑓‘𝑥) = (𝑓‘𝑦)) |
30 | | csbeq1a 3675 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → 𝑉 = ⦋𝑦 / 𝑥⦌𝑉) |
31 | 29, 30 | eleq12d 2825 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝑓‘𝑥) ∈ 𝑉 ↔ (𝑓‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉)) |
32 | 28, 31 | rspc 3435 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐼 → (∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ 𝑉 → (𝑓‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉)) |
33 | 26, 32 | mpan9 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → (𝑓‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉) |
34 | | simprr 813 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ 𝐵) |
35 | 18, 19, 21, 23, 6, 24, 34 | prdsbascl 16337 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉) |
36 | 27 | nfel2 2911 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑔‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉 |
37 | | fveq2 6344 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑔‘𝑥) = (𝑔‘𝑦)) |
38 | 37, 30 | eleq12d 2825 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝑔‘𝑥) ∈ 𝑉 ↔ (𝑔‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉)) |
39 | 36, 38 | rspc 3435 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐼 → (∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉 → (𝑔‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉)) |
40 | 35, 39 | mpan9 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → (𝑔‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉) |
41 | 33, 40 | ovresd 6958 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘𝑦)((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉))(𝑔‘𝑦)) = ((𝑓‘𝑦)(dist‘⦋𝑦 / 𝑥⦌𝑅)(𝑔‘𝑦))) |
42 | 17, 41 | eqtr4d 2789 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦)) = ((𝑓‘𝑦)((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉))(𝑔‘𝑦))) |
43 | | prdsdsf.m |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) |
44 | 43 | ralrimiva 3096 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝐸 ∈ (∞Met‘𝑉)) |
45 | 44 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 𝐸 ∈ (∞Met‘𝑉)) |
46 | | nfcv 2894 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥dist |
47 | 46, 7 | nffv 6351 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(dist‘⦋𝑦 / 𝑥⦌𝑅) |
48 | 27, 27 | nfxp 5291 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉) |
49 | 47, 48 | nfres 5545 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) |
50 | | nfcv 2894 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥∞Met |
51 | 50, 27 | nffv 6351 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(∞Met‘⦋𝑦 / 𝑥⦌𝑉) |
52 | 49, 51 | nfel 2907 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) ∈
(∞Met‘⦋𝑦 / 𝑥⦌𝑉) |
53 | | prdsdsf.e |
. . . . . . . . . . . . . . 15
⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) |
54 | 9 | fveq2d 6348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (dist‘𝑅) = (dist‘⦋𝑦 / 𝑥⦌𝑅)) |
55 | 30 | sqxpeqd 5290 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑉 × 𝑉) = (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) |
56 | 54, 55 | reseq12d 5544 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ((dist‘𝑅) ↾ (𝑉 × 𝑉)) = ((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉))) |
57 | 53, 56 | syl5eq 2798 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 𝐸 = ((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉))) |
58 | 30 | fveq2d 6348 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (∞Met‘𝑉) = (∞Met‘⦋𝑦 / 𝑥⦌𝑉)) |
59 | 57, 58 | eleq12d 2825 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐸 ∈ (∞Met‘𝑉) ↔ ((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) ∈
(∞Met‘⦋𝑦 / 𝑥⦌𝑉))) |
60 | 52, 59 | rspc 3435 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐼 → (∀𝑥 ∈ 𝐼 𝐸 ∈ (∞Met‘𝑉) → ((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) ∈
(∞Met‘⦋𝑦 / 𝑥⦌𝑉))) |
61 | 45, 60 | mpan9 487 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) ∈
(∞Met‘⦋𝑦 / 𝑥⦌𝑉)) |
62 | | xmetcl 22329 |
. . . . . . . . . . 11
⊢
((((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) ∈
(∞Met‘⦋𝑦 / 𝑥⦌𝑉) ∧ (𝑓‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉 ∧ (𝑔‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉) → ((𝑓‘𝑦)((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉))(𝑔‘𝑦)) ∈
ℝ*) |
63 | 61, 33, 40, 62 | syl3anc 1473 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘𝑦)((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉))(𝑔‘𝑦)) ∈
ℝ*) |
64 | 42, 63 | eqeltrd 2831 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦)) ∈
ℝ*) |
65 | | eqid 2752 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) = (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) |
66 | 64, 65 | fmptd 6540 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))):𝐼⟶ℝ*) |
67 | | frn 6206 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))):𝐼⟶ℝ* → ran
(𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ⊆
ℝ*) |
68 | 66, 67 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ⊆
ℝ*) |
69 | | 0xr 10270 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
70 | 69 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 0 ∈
ℝ*) |
71 | 70 | snssd 4477 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → {0} ⊆
ℝ*) |
72 | 68, 71 | unssd 3924 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}) ⊆
ℝ*) |
73 | | supxrcl 12330 |
. . . . . 6
⊢ ((ran
(𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}) ⊆ ℝ*
→ sup((ran (𝑦 ∈
𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ ℝ*) |
74 | 72, 73 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ ℝ*) |
75 | | ssun2 3912 |
. . . . . . 7
⊢ {0}
⊆ (ran (𝑦 ∈
𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}) |
76 | | c0ex 10218 |
. . . . . . . 8
⊢ 0 ∈
V |
77 | 76 | snss 4452 |
. . . . . . 7
⊢ (0 ∈
(ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}) ↔ {0} ⊆ (ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0})) |
78 | 75, 77 | mpbir 221 |
. . . . . 6
⊢ 0 ∈
(ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}) |
79 | | supxrub 12339 |
. . . . . 6
⊢ (((ran
(𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}) ⊆ ℝ*
∧ 0 ∈ (ran (𝑦
∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0})) → 0 ≤ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
)) |
80 | 72, 78, 79 | sylancl 697 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 0 ≤ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
)) |
81 | | elxrge0 12466 |
. . . . 5
⊢ (sup((ran
(𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ (0[,]+∞) ↔ (sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ ℝ* ∧ 0 ≤ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
))) |
82 | 74, 80, 81 | sylanbrc 701 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ (0[,]+∞)) |
83 | 82 | ralrimivva 3101 |
. . 3
⊢ (𝜑 → ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ (0[,]+∞)) |
84 | | eqid 2752 |
. . . 4
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < ))
= (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
)) |
85 | 84 | fmpt2 7397 |
. . 3
⊢
(∀𝑓 ∈
𝐵 ∀𝑔 ∈ 𝐵 sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ (0[,]+∞) ↔ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
)):(𝐵 × 𝐵)⟶(0[,]+∞)) |
86 | 83, 85 | sylib 208 |
. 2
⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
)):(𝐵 × 𝐵)⟶(0[,]+∞)) |
87 | | mptexg 6640 |
. . . . 5
⊢ (𝐼 ∈ 𝑋 → (𝑥 ∈ 𝐼 ↦ 𝑅) ∈ V) |
88 | 22, 87 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑅) ∈ V) |
89 | 2 | ralrimiva 3096 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑍) |
90 | | dmmptg 5785 |
. . . . 5
⊢
(∀𝑥 ∈
𝐼 𝑅 ∈ 𝑍 → dom (𝑥 ∈ 𝐼 ↦ 𝑅) = 𝐼) |
91 | 89, 90 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑥 ∈ 𝐼 ↦ 𝑅) = 𝐼) |
92 | | prdsdsf.d |
. . . 4
⊢ 𝐷 = (dist‘𝑌) |
93 | 18, 20, 88, 19, 91, 92 | prdsds 16318 |
. . 3
⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
))) |
94 | 93 | feq1d 6183 |
. 2
⊢ (𝜑 → (𝐷:(𝐵 × 𝐵)⟶(0[,]+∞) ↔ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
)):(𝐵 × 𝐵)⟶(0[,]+∞))) |
95 | 86, 94 | mpbird 247 |
1
⊢ (𝜑 → 𝐷:(𝐵 × 𝐵)⟶(0[,]+∞)) |