| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
| 2 | | prdsdsf.r |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍) |
| 3 | 2 | elexd 3504 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ V) |
| 4 | 3 | ralrimiva 3146 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ V) |
| 5 | 4 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 𝑅 ∈ V) |
| 6 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑅 |
| 7 | 6 | nfel1 2922 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑅 ∈ V |
| 8 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → 𝑅 = ⦋𝑦 / 𝑥⦌𝑅) |
| 9 | 8 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑅 ∈ V ↔ ⦋𝑦 / 𝑥⦌𝑅 ∈ V)) |
| 10 | 7, 9 | rspc 3610 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐼 → (∀𝑥 ∈ 𝐼 𝑅 ∈ V → ⦋𝑦 / 𝑥⦌𝑅 ∈ V)) |
| 11 | 5, 10 | mpan9 506 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ⦋𝑦 / 𝑥⦌𝑅 ∈ V) |
| 12 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐼 ↦ 𝑅) = (𝑥 ∈ 𝐼 ↦ 𝑅) |
| 13 | 12 | fvmpts 7019 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐼 ∧ ⦋𝑦 / 𝑥⦌𝑅 ∈ V) → ((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦) = ⦋𝑦 / 𝑥⦌𝑅) |
| 14 | 1, 11, 13 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦) = ⦋𝑦 / 𝑥⦌𝑅) |
| 15 | 14 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → (dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦)) = (dist‘⦋𝑦 / 𝑥⦌𝑅)) |
| 16 | 15 | oveqd 7448 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦)) = ((𝑓‘𝑦)(dist‘⦋𝑦 / 𝑥⦌𝑅)(𝑔‘𝑦))) |
| 17 | | prdsdsf.y |
. . . . . . . . . . . . . 14
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) |
| 18 | | prdsdsf.b |
. . . . . . . . . . . . . 14
⊢ 𝐵 = (Base‘𝑌) |
| 19 | | prdsdsf.s |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
| 20 | 19 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑆 ∈ 𝑊) |
| 21 | | prdsdsf.i |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐼 ∈ 𝑋) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝐼 ∈ 𝑋) |
| 23 | | prdsdsf.v |
. . . . . . . . . . . . . 14
⊢ 𝑉 = (Base‘𝑅) |
| 24 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑓 ∈ 𝐵) |
| 25 | 17, 18, 20, 22, 5, 23, 24 | prdsbascl 17528 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ 𝑉) |
| 26 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑉 |
| 27 | 26 | nfel2 2924 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑓‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉 |
| 28 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑓‘𝑥) = (𝑓‘𝑦)) |
| 29 | | csbeq1a 3913 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → 𝑉 = ⦋𝑦 / 𝑥⦌𝑉) |
| 30 | 28, 29 | eleq12d 2835 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝑓‘𝑥) ∈ 𝑉 ↔ (𝑓‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉)) |
| 31 | 27, 30 | rspc 3610 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐼 → (∀𝑥 ∈ 𝐼 (𝑓‘𝑥) ∈ 𝑉 → (𝑓‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉)) |
| 32 | 25, 31 | mpan9 506 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → (𝑓‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉) |
| 33 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝑔 ∈ 𝐵) |
| 34 | 17, 18, 20, 22, 5, 23, 33 | prdsbascl 17528 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉) |
| 35 | 26 | nfel2 2924 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑔‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉 |
| 36 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑔‘𝑥) = (𝑔‘𝑦)) |
| 37 | 36, 29 | eleq12d 2835 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝑔‘𝑥) ∈ 𝑉 ↔ (𝑔‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉)) |
| 38 | 35, 37 | rspc 3610 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐼 → (∀𝑥 ∈ 𝐼 (𝑔‘𝑥) ∈ 𝑉 → (𝑔‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉)) |
| 39 | 34, 38 | mpan9 506 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → (𝑔‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉) |
| 40 | 32, 39 | ovresd 7600 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘𝑦)((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉))(𝑔‘𝑦)) = ((𝑓‘𝑦)(dist‘⦋𝑦 / 𝑥⦌𝑅)(𝑔‘𝑦))) |
| 41 | 16, 40 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦)) = ((𝑓‘𝑦)((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉))(𝑔‘𝑦))) |
| 42 | | prdsdsf.m |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) |
| 43 | 42 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝐸 ∈ (∞Met‘𝑉)) |
| 44 | 43 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ∀𝑥 ∈ 𝐼 𝐸 ∈ (∞Met‘𝑉)) |
| 45 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥dist |
| 46 | 45, 6 | nffv 6916 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(dist‘⦋𝑦 / 𝑥⦌𝑅) |
| 47 | 26, 26 | nfxp 5718 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉) |
| 48 | 46, 47 | nfres 5999 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) |
| 49 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥∞Met |
| 50 | 49, 26 | nffv 6916 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(∞Met‘⦋𝑦 / 𝑥⦌𝑉) |
| 51 | 48, 50 | nfel 2920 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) ∈
(∞Met‘⦋𝑦 / 𝑥⦌𝑉) |
| 52 | | prdsdsf.e |
. . . . . . . . . . . . . . 15
⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) |
| 53 | 8 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (dist‘𝑅) = (dist‘⦋𝑦 / 𝑥⦌𝑅)) |
| 54 | 29 | sqxpeqd 5717 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑉 × 𝑉) = (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) |
| 55 | 53, 54 | reseq12d 5998 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ((dist‘𝑅) ↾ (𝑉 × 𝑉)) = ((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉))) |
| 56 | 52, 55 | eqtrid 2789 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 𝐸 = ((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉))) |
| 57 | 29 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (∞Met‘𝑉) = (∞Met‘⦋𝑦 / 𝑥⦌𝑉)) |
| 58 | 56, 57 | eleq12d 2835 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐸 ∈ (∞Met‘𝑉) ↔ ((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) ∈
(∞Met‘⦋𝑦 / 𝑥⦌𝑉))) |
| 59 | 51, 58 | rspc 3610 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐼 → (∀𝑥 ∈ 𝐼 𝐸 ∈ (∞Met‘𝑉) → ((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) ∈
(∞Met‘⦋𝑦 / 𝑥⦌𝑉))) |
| 60 | 44, 59 | mpan9 506 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) ∈
(∞Met‘⦋𝑦 / 𝑥⦌𝑉)) |
| 61 | | xmetcl 24341 |
. . . . . . . . . . 11
⊢
((((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉)) ∈
(∞Met‘⦋𝑦 / 𝑥⦌𝑉) ∧ (𝑓‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉 ∧ (𝑔‘𝑦) ∈ ⦋𝑦 / 𝑥⦌𝑉) → ((𝑓‘𝑦)((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉))(𝑔‘𝑦)) ∈
ℝ*) |
| 62 | 60, 32, 39, 61 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘𝑦)((dist‘⦋𝑦 / 𝑥⦌𝑅) ↾ (⦋𝑦 / 𝑥⦌𝑉 × ⦋𝑦 / 𝑥⦌𝑉))(𝑔‘𝑦)) ∈
ℝ*) |
| 63 | 41, 62 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) ∧ 𝑦 ∈ 𝐼) → ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦)) ∈
ℝ*) |
| 64 | 63 | fmpttd 7135 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))):𝐼⟶ℝ*) |
| 65 | 64 | frnd 6744 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ⊆
ℝ*) |
| 66 | | 0xr 11308 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
| 67 | 66 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 0 ∈
ℝ*) |
| 68 | 67 | snssd 4809 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → {0} ⊆
ℝ*) |
| 69 | 65, 68 | unssd 4192 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}) ⊆
ℝ*) |
| 70 | | supxrcl 13357 |
. . . . . 6
⊢ ((ran
(𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}) ⊆ ℝ*
→ sup((ran (𝑦 ∈
𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ ℝ*) |
| 71 | 69, 70 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ ℝ*) |
| 72 | | ssun2 4179 |
. . . . . . 7
⊢ {0}
⊆ (ran (𝑦 ∈
𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}) |
| 73 | | c0ex 11255 |
. . . . . . . 8
⊢ 0 ∈
V |
| 74 | 73 | snss 4785 |
. . . . . . 7
⊢ (0 ∈
(ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}) ↔ {0} ⊆ (ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0})) |
| 75 | 72, 74 | mpbir 231 |
. . . . . 6
⊢ 0 ∈
(ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}) |
| 76 | | supxrub 13366 |
. . . . . 6
⊢ (((ran
(𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}) ⊆ ℝ*
∧ 0 ∈ (ran (𝑦
∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0})) → 0 ≤ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
)) |
| 77 | 69, 75, 76 | sylancl 586 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 0 ≤ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
)) |
| 78 | | elxrge0 13497 |
. . . . 5
⊢ (sup((ran
(𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ (0[,]+∞) ↔ (sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ ℝ* ∧ 0 ≤ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
))) |
| 79 | 71, 77, 78 | sylanbrc 583 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ (0[,]+∞)) |
| 80 | 79 | ralrimivva 3202 |
. . 3
⊢ (𝜑 → ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ (0[,]+∞)) |
| 81 | | eqid 2737 |
. . . 4
⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < ))
= (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
)) |
| 82 | 81 | fmpo 8093 |
. . 3
⊢
(∀𝑓 ∈
𝐵 ∀𝑔 ∈ 𝐵 sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, < )
∈ (0[,]+∞) ↔ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
)):(𝐵 × 𝐵)⟶(0[,]+∞)) |
| 83 | 80, 82 | sylib 218 |
. 2
⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
)):(𝐵 × 𝐵)⟶(0[,]+∞)) |
| 84 | 21 | mptexd 7244 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑅) ∈ V) |
| 85 | 2 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑍) |
| 86 | | dmmptg 6262 |
. . . . 5
⊢
(∀𝑥 ∈
𝐼 𝑅 ∈ 𝑍 → dom (𝑥 ∈ 𝐼 ↦ 𝑅) = 𝐼) |
| 87 | 85, 86 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑥 ∈ 𝐼 ↦ 𝑅) = 𝐼) |
| 88 | | prdsdsf.d |
. . . 4
⊢ 𝐷 = (dist‘𝑌) |
| 89 | 17, 19, 84, 18, 87, 88 | prdsds 17509 |
. . 3
⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
))) |
| 90 | 89 | feq1d 6720 |
. 2
⊢ (𝜑 → (𝐷:(𝐵 × 𝐵)⟶(0[,]+∞) ↔ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑦 ∈ 𝐼 ↦ ((𝑓‘𝑦)(dist‘((𝑥 ∈ 𝐼 ↦ 𝑅)‘𝑦))(𝑔‘𝑦))) ∪ {0}), ℝ*, <
)):(𝐵 × 𝐵)⟶(0[,]+∞))) |
| 91 | 83, 90 | mpbird 257 |
1
⊢ (𝜑 → 𝐷:(𝐵 × 𝐵)⟶(0[,]+∞)) |