Proof of Theorem dvcnvrelem2
Step | Hyp | Ref
| Expression |
1 | | dvcnvre.t |
. . . . 5
⊢ 𝑇 = (topGen‘ran
(,)) |
2 | | retop 23923 |
. . . . 5
⊢
(topGen‘ran (,)) ∈ Top |
3 | 1, 2 | eqeltri 2837 |
. . . 4
⊢ 𝑇 ∈ Top |
4 | | dvcnvre.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌) |
5 | | f1ofo 6721 |
. . . . . 6
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–onto→𝑌) |
6 | | forn 6689 |
. . . . . 6
⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌) |
7 | 4, 5, 6 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ran 𝐹 = 𝑌) |
8 | | dvcnvre.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ)) |
9 | | cncff 24054 |
. . . . . 6
⊢ (𝐹 ∈ (𝑋–cn→ℝ) → 𝐹:𝑋⟶ℝ) |
10 | | frn 6605 |
. . . . . 6
⊢ (𝐹:𝑋⟶ℝ → ran 𝐹 ⊆ ℝ) |
11 | 8, 9, 10 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
12 | 7, 11 | eqsstrrd 3965 |
. . . 4
⊢ (𝜑 → 𝑌 ⊆ ℝ) |
13 | | imassrn 5979 |
. . . . 5
⊢ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ran 𝐹 |
14 | 13, 7 | sseqtrid 3978 |
. . . 4
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ 𝑌) |
15 | | uniretop 23924 |
. . . . . 6
⊢ ℝ =
∪ (topGen‘ran (,)) |
16 | 1 | unieqi 4858 |
. . . . . 6
⊢ ∪ 𝑇 =
∪ (topGen‘ran (,)) |
17 | 15, 16 | eqtr4i 2771 |
. . . . 5
⊢ ℝ =
∪ 𝑇 |
18 | 17 | ntrss 22204 |
. . . 4
⊢ ((𝑇 ∈ Top ∧ 𝑌 ⊆ ℝ ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ 𝑌) → ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ⊆ ((int‘𝑇)‘𝑌)) |
19 | 3, 12, 14, 18 | mp3an2i 1465 |
. . 3
⊢ (𝜑 → ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ⊆ ((int‘𝑇)‘𝑌)) |
20 | | dvcnvre.d |
. . . . 5
⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋) |
21 | | dvcnvre.z |
. . . . 5
⊢ (𝜑 → ¬ 0 ∈ ran
(ℝ D 𝐹)) |
22 | | dvcnvre.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
23 | | dvcnvre.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
24 | | dvcnvre.s |
. . . . 5
⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋) |
25 | 8, 20, 21, 4, 22, 23, 24 | dvcnvrelem1 25179 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘(topGen‘ran
(,)))‘(𝐹 “
((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
26 | 1 | fveq2i 6774 |
. . . . 5
⊢
(int‘𝑇) =
(int‘(topGen‘ran (,))) |
27 | 26 | fveq1i 6772 |
. . . 4
⊢
((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = ((int‘(topGen‘ran
(,)))‘(𝐹 “
((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
28 | 25, 27 | eleqtrrdi 2852 |
. . 3
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
29 | 19, 28 | sseldd 3927 |
. 2
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝑇)‘𝑌)) |
30 | | f1ocnv 6726 |
. . . . . . 7
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌–1-1-onto→𝑋) |
31 | | f1of 6714 |
. . . . . . 7
⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → ◡𝐹:𝑌⟶𝑋) |
32 | 4, 30, 31 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ◡𝐹:𝑌⟶𝑋) |
33 | | ffun 6601 |
. . . . . 6
⊢ (◡𝐹:𝑌⟶𝑋 → Fun ◡𝐹) |
34 | | funcnvres 6510 |
. . . . . 6
⊢ (Fun
◡𝐹 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
35 | 32, 33, 34 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
36 | | dvbsss 25064 |
. . . . . . . . . . 11
⊢ dom
(ℝ D 𝐹) ⊆
ℝ |
37 | 20, 36 | eqsstrrdi 3981 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
38 | | ax-resscn 10929 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
39 | 37, 38 | sstrdi 3938 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
40 | | cncfss 24060 |
. . . . . . . . 9
⊢ ((((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋 ∧ 𝑋 ⊆ ℂ) → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋)) |
41 | 24, 39, 40 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋)) |
42 | | f1of1 6713 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–1-1→𝑌) |
43 | 4, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑋–1-1→𝑌) |
44 | | f1ores 6728 |
. . . . . . . . . 10
⊢ ((𝐹:𝑋–1-1→𝑌 ∧ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋) → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
45 | 43, 24, 44 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
46 | | dvcnvre.j |
. . . . . . . . . . . . . . 15
⊢ 𝐽 =
(TopOpen‘ℂfld) |
47 | 46 | tgioo2 23964 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) = (𝐽 ↾t
ℝ) |
48 | 1, 47 | eqtri 2768 |
. . . . . . . . . . . . 13
⊢ 𝑇 = (𝐽 ↾t
ℝ) |
49 | 48 | oveq1i 7281 |
. . . . . . . . . . . 12
⊢ (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = ((𝐽 ↾t ℝ)
↾t ((𝐶
− 𝑅)[,](𝐶 + 𝑅))) |
50 | 46 | cnfldtop 23945 |
. . . . . . . . . . . . 13
⊢ 𝐽 ∈ Top |
51 | 24, 37 | sstrd 3936 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ ℝ) |
52 | | reex 10963 |
. . . . . . . . . . . . . 14
⊢ ℝ
∈ V |
53 | 52 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ∈
V) |
54 | | restabs 22314 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ ℝ ∧ ℝ ∈ V)
→ ((𝐽
↾t ℝ) ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
55 | 50, 51, 53, 54 | mp3an2i 1465 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐽 ↾t ℝ)
↾t ((𝐶
− 𝑅)[,](𝐶 + 𝑅))) = (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
56 | 49, 55 | eqtrid 2792 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
57 | 37, 22 | sseldd 3927 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℝ) |
58 | 23 | rpred 12771 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ ℝ) |
59 | 57, 58 | resubcld 11403 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 − 𝑅) ∈ ℝ) |
60 | 57, 58 | readdcld 11005 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 + 𝑅) ∈ ℝ) |
61 | | eqid 2740 |
. . . . . . . . . . . . 13
⊢ (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) |
62 | 1, 61 | icccmp 23986 |
. . . . . . . . . . . 12
⊢ (((𝐶 − 𝑅) ∈ ℝ ∧ (𝐶 + 𝑅) ∈ ℝ) → (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ Comp) |
63 | 59, 60, 62 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ Comp) |
64 | 56, 63 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ Comp) |
65 | | f1of 6714 |
. . . . . . . . . . . 12
⊢ ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))⟶(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
66 | 45, 65 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))⟶(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
67 | 11, 38 | sstrdi 3938 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝐹 ⊆ ℂ) |
68 | 13, 67 | sstrid 3937 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℂ) |
69 | | rescncf 24058 |
. . . . . . . . . . . . 13
⊢ (((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋 → (𝐹 ∈ (𝑋–cn→ℝ) → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→ℝ))) |
70 | 24, 8, 69 | sylc 65 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→ℝ)) |
71 | | cncffvrn 24059 |
. . . . . . . . . . . 12
⊢ (((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℂ ∧ (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→ℝ)) → ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ↔ (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))⟶(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
72 | 68, 70, 71 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ↔ (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))⟶(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
73 | 66, 72 | mpbird 256 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
74 | | eqid 2740 |
. . . . . . . . . . 11
⊢ (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) |
75 | 46, 74 | cncfcnvcn 24086 |
. . . . . . . . . 10
⊢ (((𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ Comp ∧ (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) → ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ↔ ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
76 | 64, 73, 75 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ↔ ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
77 | 45, 76 | mpbid 231 |
. . . . . . . 8
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
78 | 41, 77 | sseldd 3927 |
. . . . . . 7
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋)) |
79 | | eqid 2740 |
. . . . . . . . 9
⊢ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
80 | | dvcnvre.m |
. . . . . . . . 9
⊢ 𝑀 = (𝐽 ↾t 𝑋) |
81 | 46, 79, 80 | cncfcn 24071 |
. . . . . . . 8
⊢ (((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℂ ∧ 𝑋 ⊆ ℂ) → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋) = ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) Cn 𝑀)) |
82 | 68, 39, 81 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋) = ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) Cn 𝑀)) |
83 | 78, 82 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) Cn 𝑀)) |
84 | 57, 23 | ltsubrpd 12803 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 − 𝑅) < 𝐶) |
85 | 59, 57, 84 | ltled 11123 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 − 𝑅) ≤ 𝐶) |
86 | 57, 23 | ltaddrpd 12804 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 < (𝐶 + 𝑅)) |
87 | 57, 60, 86 | ltled 11123 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ≤ (𝐶 + 𝑅)) |
88 | | elicc2 13143 |
. . . . . . . . . 10
⊢ (((𝐶 − 𝑅) ∈ ℝ ∧ (𝐶 + 𝑅) ∈ ℝ) → (𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ↔ (𝐶 ∈ ℝ ∧ (𝐶 − 𝑅) ≤ 𝐶 ∧ 𝐶 ≤ (𝐶 + 𝑅)))) |
89 | 59, 60, 88 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ↔ (𝐶 ∈ ℝ ∧ (𝐶 − 𝑅) ≤ 𝐶 ∧ 𝐶 ≤ (𝐶 + 𝑅)))) |
90 | 57, 85, 87, 89 | mpbir3and 1341 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) |
91 | | ffun 6601 |
. . . . . . . . . 10
⊢ (𝐹:𝑋⟶ℝ → Fun 𝐹) |
92 | 8, 9, 91 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → Fun 𝐹) |
93 | | fdm 6607 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋⟶ℝ → dom 𝐹 = 𝑋) |
94 | 8, 9, 93 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝑋) |
95 | 24, 94 | sseqtrrd 3967 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ dom 𝐹) |
96 | | funfvima2 7104 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ dom 𝐹) → (𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) → (𝐹‘𝐶) ∈ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
97 | 92, 95, 96 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) → (𝐹‘𝐶) ∈ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
98 | 90, 97 | mpd 15 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
99 | 46 | cnfldtopon 23944 |
. . . . . . . . 9
⊢ 𝐽 ∈
(TopOn‘ℂ) |
100 | | resttopon 22310 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℂ) → (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (TopOn‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
101 | 99, 68, 100 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (TopOn‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
102 | | toponuni 22061 |
. . . . . . . 8
⊢ ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (TopOn‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
103 | 101, 102 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
104 | 98, 103 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐶) ∈ ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
105 | | eqid 2740 |
. . . . . . 7
⊢ ∪ (𝐽
↾t (𝐹
“ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
106 | 105 | cncnpi 22427 |
. . . . . 6
⊢ ((◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) Cn 𝑀) ∧ (𝐹‘𝐶) ∈ ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶))) |
107 | 83, 104, 106 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶))) |
108 | 35, 107 | eqeltrrd 2842 |
. . . 4
⊢ (𝜑 → (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶))) |
109 | | dvcnvre.n |
. . . . . . . 8
⊢ 𝑁 = (𝐽 ↾t 𝑌) |
110 | 109 | oveq1i 7281 |
. . . . . . 7
⊢ (𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = ((𝐽 ↾t 𝑌) ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
111 | | ssexg 5251 |
. . . . . . . . 9
⊢ ((𝑌 ⊆ ℝ ∧ ℝ
∈ V) → 𝑌 ∈
V) |
112 | 12, 52, 111 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ V) |
113 | | restabs 22314 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ 𝑌 ∧ 𝑌 ∈ V) → ((𝐽 ↾t 𝑌) ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
114 | 50, 14, 112, 113 | mp3an2i 1465 |
. . . . . . 7
⊢ (𝜑 → ((𝐽 ↾t 𝑌) ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
115 | 110, 114 | eqtrid 2792 |
. . . . . 6
⊢ (𝜑 → (𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
116 | 115 | oveq1d 7286 |
. . . . 5
⊢ (𝜑 → ((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀) = ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)) |
117 | 116 | fveq1d 6773 |
. . . 4
⊢ (𝜑 → (((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶)) = (((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶))) |
118 | 108, 117 | eleqtrrd 2844 |
. . 3
⊢ (𝜑 → (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶))) |
119 | 12, 38 | sstrdi 3938 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ⊆ ℂ) |
120 | | resttopon 22310 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝑌 ⊆ ℂ)
→ (𝐽
↾t 𝑌)
∈ (TopOn‘𝑌)) |
121 | 99, 119, 120 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (𝐽 ↾t 𝑌) ∈ (TopOn‘𝑌)) |
122 | 109, 121 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (TopOn‘𝑌)) |
123 | | topontop 22060 |
. . . . 5
⊢ (𝑁 ∈ (TopOn‘𝑌) → 𝑁 ∈ Top) |
124 | 122, 123 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ Top) |
125 | | toponuni 22061 |
. . . . . 6
⊢ (𝑁 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝑁) |
126 | 122, 125 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑌 = ∪ 𝑁) |
127 | 14, 126 | sseqtrd 3966 |
. . . 4
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ∪
𝑁) |
128 | 14, 12 | sstrd 3936 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℝ) |
129 | | difssd 4072 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ ∖ 𝑌) ⊆
ℝ) |
130 | 128, 129 | unssd 4125 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)) ⊆ ℝ) |
131 | | ssun1 4111 |
. . . . . . . . 9
⊢ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)) |
132 | 131 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) |
133 | 17 | ntrss 22204 |
. . . . . . . 8
⊢ ((𝑇 ∈ Top ∧ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)) ⊆ ℝ ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) → ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ⊆ ((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)))) |
134 | 3, 130, 132, 133 | mp3an2i 1465 |
. . . . . . 7
⊢ (𝜑 → ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ⊆ ((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)))) |
135 | 134, 28 | sseldd 3927 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)))) |
136 | | f1of 6714 |
. . . . . . . 8
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋⟶𝑌) |
137 | 4, 136 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
138 | 137, 22 | ffvelrnd 6959 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝑌) |
139 | 135, 138 | elind 4133 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐶) ∈ (((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) ∩ 𝑌)) |
140 | | eqid 2740 |
. . . . . . . 8
⊢ (𝑇 ↾t 𝑌) = (𝑇 ↾t 𝑌) |
141 | 17, 140 | restntr 22331 |
. . . . . . 7
⊢ ((𝑇 ∈ Top ∧ 𝑌 ⊆ ℝ ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ 𝑌) → ((int‘(𝑇 ↾t 𝑌))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) ∩ 𝑌)) |
142 | 3, 12, 14, 141 | mp3an2i 1465 |
. . . . . 6
⊢ (𝜑 → ((int‘(𝑇 ↾t 𝑌))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) ∩ 𝑌)) |
143 | | restabs 22314 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ ℝ ∧ ℝ
∈ V) → ((𝐽
↾t ℝ) ↾t 𝑌) = (𝐽 ↾t 𝑌)) |
144 | 50, 12, 53, 143 | mp3an2i 1465 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐽 ↾t ℝ)
↾t 𝑌) =
(𝐽 ↾t
𝑌)) |
145 | 48 | oveq1i 7281 |
. . . . . . . . 9
⊢ (𝑇 ↾t 𝑌) = ((𝐽 ↾t ℝ)
↾t 𝑌) |
146 | 144, 145,
109 | 3eqtr4g 2805 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ↾t 𝑌) = 𝑁) |
147 | 146 | fveq2d 6775 |
. . . . . . 7
⊢ (𝜑 → (int‘(𝑇 ↾t 𝑌)) = (int‘𝑁)) |
148 | 147 | fveq1d 6773 |
. . . . . 6
⊢ (𝜑 → ((int‘(𝑇 ↾t 𝑌))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = ((int‘𝑁)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
149 | 142, 148 | eqtr3d 2782 |
. . . . 5
⊢ (𝜑 → (((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) ∩ 𝑌) = ((int‘𝑁)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
150 | 139, 149 | eleqtrd 2843 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝑁)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
151 | 126 | feq2d 6584 |
. . . . . 6
⊢ (𝜑 → (◡𝐹:𝑌⟶𝑋 ↔ ◡𝐹:∪ 𝑁⟶𝑋)) |
152 | 32, 151 | mpbid 231 |
. . . . 5
⊢ (𝜑 → ◡𝐹:∪ 𝑁⟶𝑋) |
153 | | resttopon 22310 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝑋 ⊆ ℂ)
→ (𝐽
↾t 𝑋)
∈ (TopOn‘𝑋)) |
154 | 99, 39, 153 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (𝐽 ↾t 𝑋) ∈ (TopOn‘𝑋)) |
155 | 80, 154 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑋)) |
156 | | toponuni 22061 |
. . . . . 6
⊢ (𝑀 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑀) |
157 | | feq3 6581 |
. . . . . 6
⊢ (𝑋 = ∪
𝑀 → (◡𝐹:∪ 𝑁⟶𝑋 ↔ ◡𝐹:∪ 𝑁⟶∪ 𝑀)) |
158 | 155, 156,
157 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (◡𝐹:∪ 𝑁⟶𝑋 ↔ ◡𝐹:∪ 𝑁⟶∪ 𝑀)) |
159 | 152, 158 | mpbid 231 |
. . . 4
⊢ (𝜑 → ◡𝐹:∪ 𝑁⟶∪ 𝑀) |
160 | | eqid 2740 |
. . . . 5
⊢ ∪ 𝑁 =
∪ 𝑁 |
161 | | eqid 2740 |
. . . . 5
⊢ ∪ 𝑀 =
∪ 𝑀 |
162 | 160, 161 | cnprest 22438 |
. . . 4
⊢ (((𝑁 ∈ Top ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ∪
𝑁) ∧ ((𝐹‘𝐶) ∈ ((int‘𝑁)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∧ ◡𝐹:∪ 𝑁⟶∪ 𝑀))
→ (◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶)) ↔ (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶)))) |
163 | 124, 127,
150, 159, 162 | syl22anc 836 |
. . 3
⊢ (𝜑 → (◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶)) ↔ (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶)))) |
164 | 118, 163 | mpbird 256 |
. 2
⊢ (𝜑 → ◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶))) |
165 | 29, 164 | jca 512 |
1
⊢ (𝜑 → ((𝐹‘𝐶) ∈ ((int‘𝑇)‘𝑌) ∧ ◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶)))) |