Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. 2
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
2 | 1 | tgioo2 22414 |
. 2
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
3 | | reelprrecn 9907 |
. . 3
⊢ ℝ
∈ {ℝ, ℂ} |
4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
5 | | retop 22375 |
. . . . 5
⊢
(topGen‘ran (,)) ∈ Top |
6 | | dvcnvre.1 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌) |
7 | | f1ofo 6057 |
. . . . . . 7
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–onto→𝑌) |
8 | | forn 6031 |
. . . . . . 7
⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌) |
9 | 6, 7, 8 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 = 𝑌) |
10 | | dvcnvre.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ)) |
11 | | cncff 22504 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑋–cn→ℝ) → 𝐹:𝑋⟶ℝ) |
12 | | frn 5966 |
. . . . . . 7
⊢ (𝐹:𝑋⟶ℝ → ran 𝐹 ⊆ ℝ) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
14 | 9, 13 | eqsstr3d 3603 |
. . . . 5
⊢ (𝜑 → 𝑌 ⊆ ℝ) |
15 | | uniretop 22376 |
. . . . . 6
⊢ ℝ =
∪ (topGen‘ran (,)) |
16 | 15 | ntrss2 20671 |
. . . . 5
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝑌 ⊆ ℝ) →
((int‘(topGen‘ran (,)))‘𝑌) ⊆ 𝑌) |
17 | 5, 14, 16 | sylancr 694 |
. . . 4
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘𝑌) ⊆ 𝑌) |
18 | | f1ocnvfv2 6433 |
. . . . . . . 8
⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
19 | 6, 18 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
20 | | f1ocnv 6062 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌–1-1-onto→𝑋) |
21 | | f1of 6050 |
. . . . . . . . . . . 12
⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → ◡𝐹:𝑌⟶𝑋) |
22 | 6, 20, 21 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝐹:𝑌⟶𝑋) |
23 | 22 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (◡𝐹‘𝑥) ∈ 𝑋) |
24 | | dvcnvre.d |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋) |
25 | | dvbsss 23472 |
. . . . . . . . . . . . . . . 16
⊢ dom
(ℝ D 𝐹) ⊆
ℝ |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (ℝ D 𝐹) ⊆
ℝ) |
27 | 24, 26 | eqsstr3d 3603 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
28 | 15 | ntrss2 20671 |
. . . . . . . . . . . . . 14
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝑋 ⊆ ℝ) →
((int‘(topGen‘ran (,)))‘𝑋) ⊆ 𝑋) |
29 | 5, 27, 28 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘𝑋) ⊆ 𝑋) |
30 | | ax-resscn 9872 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
⊆ ℂ |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ℝ ⊆
ℂ) |
32 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
33 | | fss 5969 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑋⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:𝑋⟶ℂ) |
34 | 32, 30, 33 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
35 | 31, 34, 27, 2, 1 | dvbssntr 23470 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (ℝ D 𝐹) ⊆
((int‘(topGen‘ran (,)))‘𝑋)) |
36 | 24, 35 | eqsstr3d 3603 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ⊆ ((int‘(topGen‘ran
(,)))‘𝑋)) |
37 | 29, 36 | eqssd 3585 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘𝑋) = 𝑋) |
38 | 15 | isopn3 20680 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝑋 ⊆ ℝ) → (𝑋 ∈ (topGen‘ran (,)) ↔
((int‘(topGen‘ran (,)))‘𝑋) = 𝑋)) |
39 | 5, 27, 38 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ∈ (topGen‘ran (,)) ↔
((int‘(topGen‘ran (,)))‘𝑋) = 𝑋)) |
40 | 37, 39 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (topGen‘ran
(,))) |
41 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
42 | 41 | rexmet 22402 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
43 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
44 | 41, 43 | tgioo 22407 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
45 | 44 | mopni2 22108 |
. . . . . . . . . . . 12
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ 𝑋 ∈ (topGen‘ran (,)) ∧ (◡𝐹‘𝑥) ∈ 𝑋) → ∃𝑟 ∈ ℝ+ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋) |
46 | 42, 45 | mp3an1 1403 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ (topGen‘ran (,))
∧ (◡𝐹‘𝑥) ∈ 𝑋) → ∃𝑟 ∈ ℝ+ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋) |
47 | 40, 46 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (◡𝐹‘𝑥) ∈ 𝑋) → ∃𝑟 ∈ ℝ+ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋) |
48 | 23, 47 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ∃𝑟 ∈ ℝ+ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋) |
49 | 10 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → 𝐹 ∈ (𝑋–cn→ℝ)) |
50 | 24 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → dom (ℝ D 𝐹) = 𝑋) |
51 | | dvcnvre.z |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 0 ∈ ran
(ℝ D 𝐹)) |
52 | 51 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ¬ 0 ∈ ran (ℝ D
𝐹)) |
53 | 6 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → 𝐹:𝑋–1-1-onto→𝑌) |
54 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (◡𝐹‘𝑥) ∈ 𝑋) |
55 | | rphalfcl 11734 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ+) |
56 | 55 | ad2antrl 760 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (𝑟 / 2) ∈
ℝ+) |
57 | 27 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → 𝑋 ⊆ ℝ) |
58 | 57, 54 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (◡𝐹‘𝑥) ∈ ℝ) |
59 | 56 | rpred 11748 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (𝑟 / 2) ∈ ℝ) |
60 | 58, 59 | resubcld 10337 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((◡𝐹‘𝑥) − (𝑟 / 2)) ∈ ℝ) |
61 | 58, 59 | readdcld 9948 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((◡𝐹‘𝑥) + (𝑟 / 2)) ∈ ℝ) |
62 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((◡𝐹‘𝑥) − (𝑟 / 2)) ∈ ℝ ∧ ((◡𝐹‘𝑥) + (𝑟 / 2)) ∈ ℝ) → (𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2))) ↔ (𝑦 ∈ ℝ ∧ ((◡𝐹‘𝑥) − (𝑟 / 2)) ≤ 𝑦 ∧ 𝑦 ≤ ((◡𝐹‘𝑥) + (𝑟 / 2))))) |
63 | 60, 61, 62 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2))) ↔ (𝑦 ∈ ℝ ∧ ((◡𝐹‘𝑥) − (𝑟 / 2)) ≤ 𝑦 ∧ 𝑦 ≤ ((◡𝐹‘𝑥) + (𝑟 / 2))))) |
64 | 63 | biimpa 500 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑦 ∈ ℝ ∧ ((◡𝐹‘𝑥) − (𝑟 / 2)) ≤ 𝑦 ∧ 𝑦 ≤ ((◡𝐹‘𝑥) + (𝑟 / 2)))) |
65 | 64 | simp1d 1066 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑦 ∈ ℝ) |
66 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → (◡𝐹‘𝑥) ∈ ℝ) |
67 | | simplrl 796 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑟 ∈ ℝ+) |
68 | 67 | rpred 11748 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑟 ∈ ℝ) |
69 | 66, 68 | resubcld 10337 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → ((◡𝐹‘𝑥) − 𝑟) ∈ ℝ) |
70 | 60 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → ((◡𝐹‘𝑥) − (𝑟 / 2)) ∈ ℝ) |
71 | 67, 55 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑟 / 2) ∈
ℝ+) |
72 | 71 | rpred 11748 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑟 / 2) ∈ ℝ) |
73 | | rphalflt 11736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) < 𝑟) |
74 | 67, 73 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑟 / 2) < 𝑟) |
75 | 72, 68, 66, 74 | ltsub2dd 10519 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → ((◡𝐹‘𝑥) − 𝑟) < ((◡𝐹‘𝑥) − (𝑟 / 2))) |
76 | 64 | simp2d 1067 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → ((◡𝐹‘𝑥) − (𝑟 / 2)) ≤ 𝑦) |
77 | 69, 70, 65, 75, 76 | ltletrd 10076 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → ((◡𝐹‘𝑥) − 𝑟) < 𝑦) |
78 | 61 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → ((◡𝐹‘𝑥) + (𝑟 / 2)) ∈ ℝ) |
79 | 66, 68 | readdcld 9948 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → ((◡𝐹‘𝑥) + 𝑟) ∈ ℝ) |
80 | 64 | simp3d 1068 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑦 ≤ ((◡𝐹‘𝑥) + (𝑟 / 2))) |
81 | 72, 68, 66, 74 | ltadd2dd 10075 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → ((◡𝐹‘𝑥) + (𝑟 / 2)) < ((◡𝐹‘𝑥) + 𝑟)) |
82 | 65, 78, 79, 80, 81 | lelttrd 10074 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑦 < ((◡𝐹‘𝑥) + 𝑟)) |
83 | 69 | rexrd 9968 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → ((◡𝐹‘𝑥) − 𝑟) ∈
ℝ*) |
84 | 79 | rexrd 9968 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → ((◡𝐹‘𝑥) + 𝑟) ∈
ℝ*) |
85 | | elioo2 12087 |
. . . . . . . . . . . . . . . 16
⊢ ((((◡𝐹‘𝑥) − 𝑟) ∈ ℝ* ∧ ((◡𝐹‘𝑥) + 𝑟) ∈ ℝ*) → (𝑦 ∈ (((◡𝐹‘𝑥) − 𝑟)(,)((◡𝐹‘𝑥) + 𝑟)) ↔ (𝑦 ∈ ℝ ∧ ((◡𝐹‘𝑥) − 𝑟) < 𝑦 ∧ 𝑦 < ((◡𝐹‘𝑥) + 𝑟)))) |
86 | 83, 84, 85 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → (𝑦 ∈ (((◡𝐹‘𝑥) − 𝑟)(,)((◡𝐹‘𝑥) + 𝑟)) ↔ (𝑦 ∈ ℝ ∧ ((◡𝐹‘𝑥) − 𝑟) < 𝑦 ∧ 𝑦 < ((◡𝐹‘𝑥) + 𝑟)))) |
87 | 65, 77, 82, 86 | mpbir3and 1238 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) ∧ 𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2)))) → 𝑦 ∈ (((◡𝐹‘𝑥) − 𝑟)(,)((◡𝐹‘𝑥) + 𝑟))) |
88 | 87 | ex 449 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (𝑦 ∈ (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2))) → 𝑦 ∈ (((◡𝐹‘𝑥) − 𝑟)(,)((◡𝐹‘𝑥) + 𝑟)))) |
89 | 88 | ssrdv 3574 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2))) ⊆ (((◡𝐹‘𝑥) − 𝑟)(,)((◡𝐹‘𝑥) + 𝑟))) |
90 | | rpre 11715 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
91 | 90 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → 𝑟 ∈ ℝ) |
92 | 41 | bl2ioo 22403 |
. . . . . . . . . . . . 13
⊢ (((◡𝐹‘𝑥) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) = (((◡𝐹‘𝑥) − 𝑟)(,)((◡𝐹‘𝑥) + 𝑟))) |
93 | 58, 91, 92 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) = (((◡𝐹‘𝑥) − 𝑟)(,)((◡𝐹‘𝑥) + 𝑟))) |
94 | 89, 93 | sseqtr4d 3605 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2))) ⊆ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟)) |
95 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋) |
96 | 94, 95 | sstrd 3578 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → (((◡𝐹‘𝑥) − (𝑟 / 2))[,]((◡𝐹‘𝑥) + (𝑟 / 2))) ⊆ 𝑋) |
97 | | eqid 2610 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
98 | | eqid 2610 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t 𝑋) =
((TopOpen‘ℂfld) ↾t 𝑋) |
99 | | eqid 2610 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t 𝑌) =
((TopOpen‘ℂfld) ↾t 𝑌) |
100 | 49, 50, 52, 53, 54, 56, 96, 97, 1, 98, 99 | dvcnvrelem2 23585 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑌) ∧ (𝑟 ∈ ℝ+ ∧ ((◡𝐹‘𝑥)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑟) ⊆ 𝑋)) → ((𝐹‘(◡𝐹‘𝑥)) ∈ ((int‘(topGen‘ran
(,)))‘𝑌) ∧ ◡𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑌) CnP ((TopOpen‘ℂfld)
↾t 𝑋))‘(𝐹‘(◡𝐹‘𝑥))))) |
101 | 48, 100 | rexlimddv 3017 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝐹‘(◡𝐹‘𝑥)) ∈ ((int‘(topGen‘ran
(,)))‘𝑌) ∧ ◡𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑌) CnP ((TopOpen‘ℂfld)
↾t 𝑋))‘(𝐹‘(◡𝐹‘𝑥))))) |
102 | 101 | simpld 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐹‘(◡𝐹‘𝑥)) ∈ ((int‘(topGen‘ran
(,)))‘𝑌)) |
103 | 19, 102 | eqeltrrd 2689 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ ((int‘(topGen‘ran
(,)))‘𝑌)) |
104 | 103 | ex 449 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑌 → 𝑥 ∈ ((int‘(topGen‘ran
(,)))‘𝑌))) |
105 | 104 | ssrdv 3574 |
. . . 4
⊢ (𝜑 → 𝑌 ⊆ ((int‘(topGen‘ran
(,)))‘𝑌)) |
106 | 17, 105 | eqssd 3585 |
. . 3
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘𝑌) = 𝑌) |
107 | 15 | isopn3 20680 |
. . . 4
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝑌 ⊆ ℝ) → (𝑌 ∈ (topGen‘ran (,)) ↔
((int‘(topGen‘ran (,)))‘𝑌) = 𝑌)) |
108 | 5, 14, 107 | sylancr 694 |
. . 3
⊢ (𝜑 → (𝑌 ∈ (topGen‘ran (,)) ↔
((int‘(topGen‘ran (,)))‘𝑌) = 𝑌)) |
109 | 106, 108 | mpbird 246 |
. 2
⊢ (𝜑 → 𝑌 ∈ (topGen‘ran
(,))) |
110 | 101 | simprd 478 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ◡𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑌) CnP ((TopOpen‘ℂfld)
↾t 𝑋))‘(𝐹‘(◡𝐹‘𝑥)))) |
111 | 19 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) →
((((TopOpen‘ℂfld) ↾t 𝑌) CnP ((TopOpen‘ℂfld)
↾t 𝑋))‘(𝐹‘(◡𝐹‘𝑥))) =
((((TopOpen‘ℂfld) ↾t 𝑌) CnP ((TopOpen‘ℂfld)
↾t 𝑋))‘𝑥)) |
112 | 110, 111 | eleqtrd 2690 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ◡𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑌) CnP ((TopOpen‘ℂfld)
↾t 𝑋))‘𝑥)) |
113 | 112 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑌 ◡𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑌) CnP ((TopOpen‘ℂfld)
↾t 𝑋))‘𝑥)) |
114 | 1 | cnfldtopon 22396 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
115 | 14, 30 | syl6ss 3580 |
. . . . . 6
⊢ (𝜑 → 𝑌 ⊆ ℂ) |
116 | | resttopon 20775 |
. . . . . 6
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑌 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑌) ∈ (TopOn‘𝑌)) |
117 | 114, 115,
116 | sylancr 694 |
. . . . 5
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝑌) ∈ (TopOn‘𝑌)) |
118 | 27, 30 | syl6ss 3580 |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
119 | | resttopon 20775 |
. . . . . 6
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑋 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑋) ∈ (TopOn‘𝑋)) |
120 | 114, 118,
119 | sylancr 694 |
. . . . 5
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝑋) ∈ (TopOn‘𝑋)) |
121 | | cncnp 20894 |
. . . . 5
⊢
((((TopOpen‘ℂfld) ↾t 𝑌) ∈ (TopOn‘𝑌) ∧
((TopOpen‘ℂfld) ↾t 𝑋) ∈ (TopOn‘𝑋)) → (◡𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑌) Cn ((TopOpen‘ℂfld)
↾t 𝑋))
↔ (◡𝐹:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑌 ◡𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑌) CnP ((TopOpen‘ℂfld)
↾t 𝑋))‘𝑥)))) |
122 | 117, 120,
121 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (◡𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑌) Cn ((TopOpen‘ℂfld)
↾t 𝑋))
↔ (◡𝐹:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑌 ◡𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑌) CnP ((TopOpen‘ℂfld)
↾t 𝑋))‘𝑥)))) |
123 | 22, 113, 122 | mpbir2and 959 |
. . 3
⊢ (𝜑 → ◡𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑌) Cn ((TopOpen‘ℂfld)
↾t 𝑋))) |
124 | 1, 99, 98 | cncfcn 22520 |
. . . 4
⊢ ((𝑌 ⊆ ℂ ∧ 𝑋 ⊆ ℂ) → (𝑌–cn→𝑋) = (((TopOpen‘ℂfld)
↾t 𝑌) Cn
((TopOpen‘ℂfld) ↾t 𝑋))) |
125 | 115, 118,
124 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑌–cn→𝑋) = (((TopOpen‘ℂfld)
↾t 𝑌) Cn
((TopOpen‘ℂfld) ↾t 𝑋))) |
126 | 123, 125 | eleqtrrd 2691 |
. 2
⊢ (𝜑 → ◡𝐹 ∈ (𝑌–cn→𝑋)) |
127 | 1, 2, 4, 109, 6, 126, 24, 51 | dvcnv 23544 |
1
⊢ (𝜑 → (ℝ D ◡𝐹) = (𝑥 ∈ 𝑌 ↦ (1 / ((ℝ D 𝐹)‘(◡𝐹‘𝑥))))) |