Step | Hyp | Ref
| Expression |
1 | | metdscn.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, <
)) |
2 | 1 | metdsf 23600 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
3 | | iccssxr 12904 |
. . 3
⊢
(0[,]+∞) ⊆ ℝ* |
4 | | fss 6521 |
. . 3
⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ (0[,]+∞)
⊆ ℝ*) → 𝐹:𝑋⟶ℝ*) |
5 | 2, 3, 4 | sylancl 589 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶ℝ*) |
6 | | simprr 773 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → 𝑟 ∈
ℝ+) |
7 | 5 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → 𝐹:𝑋⟶ℝ*) |
8 | | simplrl 777 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → 𝑧 ∈ 𝑋) |
9 | 7, 8 | ffvelrnd 6862 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → (𝐹‘𝑧) ∈
ℝ*) |
10 | | simprl 771 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → 𝑤 ∈ 𝑋) |
11 | 7, 10 | ffvelrnd 6862 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → (𝐹‘𝑤) ∈
ℝ*) |
12 | | metdscn.c |
. . . . . . . . 9
⊢ 𝐶 =
(dist‘ℝ*𝑠) |
13 | 12 | xrsdsval 20261 |
. . . . . . . 8
⊢ (((𝐹‘𝑧) ∈ ℝ* ∧ (𝐹‘𝑤) ∈ ℝ*) → ((𝐹‘𝑧)𝐶(𝐹‘𝑤)) = if((𝐹‘𝑧) ≤ (𝐹‘𝑤), ((𝐹‘𝑤) +𝑒
-𝑒(𝐹‘𝑧)), ((𝐹‘𝑧) +𝑒
-𝑒(𝐹‘𝑤)))) |
14 | 9, 11, 13 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → ((𝐹‘𝑧)𝐶(𝐹‘𝑤)) = if((𝐹‘𝑧) ≤ (𝐹‘𝑤), ((𝐹‘𝑤) +𝑒
-𝑒(𝐹‘𝑧)), ((𝐹‘𝑧) +𝑒
-𝑒(𝐹‘𝑤)))) |
15 | | metdscn.j |
. . . . . . . . 9
⊢ 𝐽 = (MetOpen‘𝐷) |
16 | | metdscn.k |
. . . . . . . . 9
⊢ 𝐾 = (MetOpen‘𝐶) |
17 | | simplll 775 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → 𝐷 ∈ (∞Met‘𝑋)) |
18 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → 𝑆 ⊆ 𝑋) |
19 | | simplrr 778 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → 𝑟 ∈ ℝ+) |
20 | | xmetsym 23100 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑤 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑤𝐷𝑧) = (𝑧𝐷𝑤)) |
21 | 17, 10, 8, 20 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → (𝑤𝐷𝑧) = (𝑧𝐷𝑤)) |
22 | | simprr 773 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → (𝑧𝐷𝑤) < 𝑟) |
23 | 21, 22 | eqbrtrd 5052 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → (𝑤𝐷𝑧) < 𝑟) |
24 | 1, 15, 12, 16, 17, 18, 10, 8, 19, 23 | metdscnlem 23607 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → ((𝐹‘𝑤) +𝑒
-𝑒(𝐹‘𝑧)) < 𝑟) |
25 | 1, 15, 12, 16, 17, 18, 8, 10, 19, 22 | metdscnlem 23607 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → ((𝐹‘𝑧) +𝑒
-𝑒(𝐹‘𝑤)) < 𝑟) |
26 | | breq1 5033 |
. . . . . . . . 9
⊢ (((𝐹‘𝑤) +𝑒
-𝑒(𝐹‘𝑧)) = if((𝐹‘𝑧) ≤ (𝐹‘𝑤), ((𝐹‘𝑤) +𝑒
-𝑒(𝐹‘𝑧)), ((𝐹‘𝑧) +𝑒
-𝑒(𝐹‘𝑤))) → (((𝐹‘𝑤) +𝑒
-𝑒(𝐹‘𝑧)) < 𝑟 ↔ if((𝐹‘𝑧) ≤ (𝐹‘𝑤), ((𝐹‘𝑤) +𝑒
-𝑒(𝐹‘𝑧)), ((𝐹‘𝑧) +𝑒
-𝑒(𝐹‘𝑤))) < 𝑟)) |
27 | | breq1 5033 |
. . . . . . . . 9
⊢ (((𝐹‘𝑧) +𝑒
-𝑒(𝐹‘𝑤)) = if((𝐹‘𝑧) ≤ (𝐹‘𝑤), ((𝐹‘𝑤) +𝑒
-𝑒(𝐹‘𝑧)), ((𝐹‘𝑧) +𝑒
-𝑒(𝐹‘𝑤))) → (((𝐹‘𝑧) +𝑒
-𝑒(𝐹‘𝑤)) < 𝑟 ↔ if((𝐹‘𝑧) ≤ (𝐹‘𝑤), ((𝐹‘𝑤) +𝑒
-𝑒(𝐹‘𝑧)), ((𝐹‘𝑧) +𝑒
-𝑒(𝐹‘𝑤))) < 𝑟)) |
28 | 26, 27 | ifboth 4453 |
. . . . . . . 8
⊢ ((((𝐹‘𝑤) +𝑒
-𝑒(𝐹‘𝑧)) < 𝑟 ∧ ((𝐹‘𝑧) +𝑒
-𝑒(𝐹‘𝑤)) < 𝑟) → if((𝐹‘𝑧) ≤ (𝐹‘𝑤), ((𝐹‘𝑤) +𝑒
-𝑒(𝐹‘𝑧)), ((𝐹‘𝑧) +𝑒
-𝑒(𝐹‘𝑤))) < 𝑟) |
29 | 24, 25, 28 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → if((𝐹‘𝑧) ≤ (𝐹‘𝑤), ((𝐹‘𝑤) +𝑒
-𝑒(𝐹‘𝑧)), ((𝐹‘𝑧) +𝑒
-𝑒(𝐹‘𝑤))) < 𝑟) |
30 | 14, 29 | eqbrtrd 5052 |
. . . . . 6
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ (𝑤 ∈ 𝑋 ∧ (𝑧𝐷𝑤) < 𝑟)) → ((𝐹‘𝑧)𝐶(𝐹‘𝑤)) < 𝑟) |
31 | 30 | expr 460 |
. . . . 5
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) ∧ 𝑤 ∈ 𝑋) → ((𝑧𝐷𝑤) < 𝑟 → ((𝐹‘𝑧)𝐶(𝐹‘𝑤)) < 𝑟)) |
32 | 31 | ralrimiva 3096 |
. . . 4
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) →
∀𝑤 ∈ 𝑋 ((𝑧𝐷𝑤) < 𝑟 → ((𝐹‘𝑧)𝐶(𝐹‘𝑤)) < 𝑟)) |
33 | | breq2 5034 |
. . . . 5
⊢ (𝑠 = 𝑟 → ((𝑧𝐷𝑤) < 𝑠 ↔ (𝑧𝐷𝑤) < 𝑟)) |
34 | 33 | rspceaimv 3531 |
. . . 4
⊢ ((𝑟 ∈ ℝ+
∧ ∀𝑤 ∈
𝑋 ((𝑧𝐷𝑤) < 𝑟 → ((𝐹‘𝑧)𝐶(𝐹‘𝑤)) < 𝑟)) → ∃𝑠 ∈ ℝ+ ∀𝑤 ∈ 𝑋 ((𝑧𝐷𝑤) < 𝑠 → ((𝐹‘𝑧)𝐶(𝐹‘𝑤)) < 𝑟)) |
35 | 6, 32, 34 | syl2anc 587 |
. . 3
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) →
∃𝑠 ∈
ℝ+ ∀𝑤 ∈ 𝑋 ((𝑧𝐷𝑤) < 𝑠 → ((𝐹‘𝑧)𝐶(𝐹‘𝑤)) < 𝑟)) |
36 | 35 | ralrimivva 3103 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → ∀𝑧 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
∀𝑤 ∈ 𝑋 ((𝑧𝐷𝑤) < 𝑠 → ((𝐹‘𝑧)𝐶(𝐹‘𝑤)) < 𝑟)) |
37 | | simpl 486 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
38 | 12 | xrsxmet 23561 |
. . 3
⊢ 𝐶 ∈
(∞Met‘ℝ*) |
39 | 15, 16 | metcn 23296 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐶 ∈
(∞Met‘ℝ*)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶ℝ* ∧
∀𝑧 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
∀𝑤 ∈ 𝑋 ((𝑧𝐷𝑤) < 𝑠 → ((𝐹‘𝑧)𝐶(𝐹‘𝑤)) < 𝑟)))) |
40 | 37, 38, 39 | sylancl 589 |
. 2
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶ℝ* ∧
∀𝑧 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
∀𝑤 ∈ 𝑋 ((𝑧𝐷𝑤) < 𝑠 → ((𝐹‘𝑧)𝐶(𝐹‘𝑤)) < 𝑟)))) |
41 | 5, 36, 40 | mpbir2and 713 |
1
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐾)) |