Proof of Theorem dvcnvrelem2
Step | Hyp | Ref
| Expression |
1 | | dvcnvre.t |
. . . . . 6
⊢ 𝑇 = (topGen‘ran
(,)) |
2 | | retop 22973 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ Top |
3 | 1, 2 | eqeltri 2855 |
. . . . 5
⊢ 𝑇 ∈ Top |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ Top) |
5 | | dvcnvre.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌) |
6 | | f1ofo 6398 |
. . . . . 6
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–onto→𝑌) |
7 | | forn 6369 |
. . . . . 6
⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌) |
8 | 5, 6, 7 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ran 𝐹 = 𝑌) |
9 | | dvcnvre.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ)) |
10 | | cncff 23104 |
. . . . . 6
⊢ (𝐹 ∈ (𝑋–cn→ℝ) → 𝐹:𝑋⟶ℝ) |
11 | | frn 6297 |
. . . . . 6
⊢ (𝐹:𝑋⟶ℝ → ran 𝐹 ⊆ ℝ) |
12 | 9, 10, 11 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
13 | 8, 12 | eqsstr3d 3859 |
. . . 4
⊢ (𝜑 → 𝑌 ⊆ ℝ) |
14 | | imassrn 5731 |
. . . . 5
⊢ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ran 𝐹 |
15 | 14, 8 | syl5sseq 3872 |
. . . 4
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ 𝑌) |
16 | | uniretop 22974 |
. . . . . 6
⊢ ℝ =
∪ (topGen‘ran (,)) |
17 | 1 | unieqi 4680 |
. . . . . 6
⊢ ∪ 𝑇 =
∪ (topGen‘ran (,)) |
18 | 16, 17 | eqtr4i 2805 |
. . . . 5
⊢ ℝ =
∪ 𝑇 |
19 | 18 | ntrss 21267 |
. . . 4
⊢ ((𝑇 ∈ Top ∧ 𝑌 ⊆ ℝ ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ 𝑌) → ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ⊆ ((int‘𝑇)‘𝑌)) |
20 | 4, 13, 15, 19 | syl3anc 1439 |
. . 3
⊢ (𝜑 → ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ⊆ ((int‘𝑇)‘𝑌)) |
21 | | dvcnvre.d |
. . . . 5
⊢ (𝜑 → dom (ℝ D 𝐹) = 𝑋) |
22 | | dvcnvre.z |
. . . . 5
⊢ (𝜑 → ¬ 0 ∈ ran
(ℝ D 𝐹)) |
23 | | dvcnvre.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
24 | | dvcnvre.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
25 | | dvcnvre.s |
. . . . 5
⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋) |
26 | 9, 21, 22, 5, 23, 24, 25 | dvcnvrelem1 24217 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘(topGen‘ran
(,)))‘(𝐹 “
((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
27 | 1 | fveq2i 6449 |
. . . . 5
⊢
(int‘𝑇) =
(int‘(topGen‘ran (,))) |
28 | 27 | fveq1i 6447 |
. . . 4
⊢
((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = ((int‘(topGen‘ran
(,)))‘(𝐹 “
((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
29 | 26, 28 | syl6eleqr 2870 |
. . 3
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
30 | 20, 29 | sseldd 3822 |
. 2
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝑇)‘𝑌)) |
31 | | f1ocnv 6403 |
. . . . . . 7
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌–1-1-onto→𝑋) |
32 | | f1of 6391 |
. . . . . . 7
⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → ◡𝐹:𝑌⟶𝑋) |
33 | 5, 31, 32 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ◡𝐹:𝑌⟶𝑋) |
34 | | ffun 6294 |
. . . . . 6
⊢ (◡𝐹:𝑌⟶𝑋 → Fun ◡𝐹) |
35 | | funcnvres 6212 |
. . . . . 6
⊢ (Fun
◡𝐹 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
36 | 33, 34, 35 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
37 | | dvbsss 24103 |
. . . . . . . . . . 11
⊢ dom
(ℝ D 𝐹) ⊆
ℝ |
38 | 21, 37 | syl6eqssr 3875 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
39 | | ax-resscn 10329 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
40 | 38, 39 | syl6ss 3833 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
41 | | cncfss 23110 |
. . . . . . . . 9
⊢ ((((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋 ∧ 𝑋 ⊆ ℂ) → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋)) |
42 | 25, 40, 41 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋)) |
43 | | f1of1 6390 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–1-1→𝑌) |
44 | 5, 43 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑋–1-1→𝑌) |
45 | | f1ores 6405 |
. . . . . . . . . 10
⊢ ((𝐹:𝑋–1-1→𝑌 ∧ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋) → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
46 | 44, 25, 45 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
47 | | dvcnvre.j |
. . . . . . . . . . . . . . 15
⊢ 𝐽 =
(TopOpen‘ℂfld) |
48 | 47 | tgioo2 23014 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) = (𝐽 ↾t
ℝ) |
49 | 1, 48 | eqtri 2802 |
. . . . . . . . . . . . 13
⊢ 𝑇 = (𝐽 ↾t
ℝ) |
50 | 49 | oveq1i 6932 |
. . . . . . . . . . . 12
⊢ (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = ((𝐽 ↾t ℝ)
↾t ((𝐶
− 𝑅)[,](𝐶 + 𝑅))) |
51 | 47 | cnfldtop 22995 |
. . . . . . . . . . . . . 14
⊢ 𝐽 ∈ Top |
52 | 51 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ Top) |
53 | 25, 38 | sstrd 3831 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ ℝ) |
54 | | reex 10363 |
. . . . . . . . . . . . . 14
⊢ ℝ
∈ V |
55 | 54 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ∈
V) |
56 | | restabs 21377 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ ℝ ∧ ℝ ∈ V)
→ ((𝐽
↾t ℝ) ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
57 | 52, 53, 55, 56 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐽 ↾t ℝ)
↾t ((𝐶
− 𝑅)[,](𝐶 + 𝑅))) = (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
58 | 50, 57 | syl5eq 2826 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
59 | 38, 23 | sseldd 3822 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℝ) |
60 | 24 | rpred 12181 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ ℝ) |
61 | 59, 60 | resubcld 10803 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 − 𝑅) ∈ ℝ) |
62 | 59, 60 | readdcld 10406 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 + 𝑅) ∈ ℝ) |
63 | | eqid 2778 |
. . . . . . . . . . . . 13
⊢ (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) |
64 | 1, 63 | icccmp 23036 |
. . . . . . . . . . . 12
⊢ (((𝐶 − 𝑅) ∈ ℝ ∧ (𝐶 + 𝑅) ∈ ℝ) → (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ Comp) |
65 | 61, 62, 64 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ Comp) |
66 | 58, 65 | eqeltrrd 2860 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ Comp) |
67 | | f1of 6391 |
. . . . . . . . . . . 12
⊢ ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))⟶(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
68 | 46, 67 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))⟶(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
69 | 12, 39 | syl6ss 3833 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝐹 ⊆ ℂ) |
70 | 14, 69 | syl5ss 3832 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℂ) |
71 | | rescncf 23108 |
. . . . . . . . . . . . 13
⊢ (((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋 → (𝐹 ∈ (𝑋–cn→ℝ) → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→ℝ))) |
72 | 25, 9, 71 | sylc 65 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→ℝ)) |
73 | | cncffvrn 23109 |
. . . . . . . . . . . 12
⊢ (((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℂ ∧ (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→ℝ)) → ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ↔ (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))⟶(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
74 | 70, 72, 73 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ↔ (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))⟶(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
75 | 68, 74 | mpbird 249 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
76 | | eqid 2778 |
. . . . . . . . . . 11
⊢ (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) |
77 | 47, 76 | cncfcnvcn 23132 |
. . . . . . . . . 10
⊢ (((𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ Comp ∧ (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) → ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ↔ ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
78 | 66, 75, 77 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ↔ ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
79 | 46, 78 | mpbid 224 |
. . . . . . . 8
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
80 | 42, 79 | sseldd 3822 |
. . . . . . 7
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋)) |
81 | | eqid 2778 |
. . . . . . . . 9
⊢ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
82 | | dvcnvre.m |
. . . . . . . . 9
⊢ 𝑀 = (𝐽 ↾t 𝑋) |
83 | 47, 81, 82 | cncfcn 23120 |
. . . . . . . 8
⊢ (((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℂ ∧ 𝑋 ⊆ ℂ) → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋) = ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) Cn 𝑀)) |
84 | 70, 40, 83 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋) = ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) Cn 𝑀)) |
85 | 80, 84 | eleqtrd 2861 |
. . . . . 6
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) Cn 𝑀)) |
86 | 59, 24 | ltsubrpd 12213 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 − 𝑅) < 𝐶) |
87 | 61, 59, 86 | ltled 10524 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 − 𝑅) ≤ 𝐶) |
88 | 59, 24 | ltaddrpd 12214 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 < (𝐶 + 𝑅)) |
89 | 59, 62, 88 | ltled 10524 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ≤ (𝐶 + 𝑅)) |
90 | | elicc2 12550 |
. . . . . . . . . 10
⊢ (((𝐶 − 𝑅) ∈ ℝ ∧ (𝐶 + 𝑅) ∈ ℝ) → (𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ↔ (𝐶 ∈ ℝ ∧ (𝐶 − 𝑅) ≤ 𝐶 ∧ 𝐶 ≤ (𝐶 + 𝑅)))) |
91 | 61, 62, 90 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ↔ (𝐶 ∈ ℝ ∧ (𝐶 − 𝑅) ≤ 𝐶 ∧ 𝐶 ≤ (𝐶 + 𝑅)))) |
92 | 59, 87, 89, 91 | mpbir3and 1399 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) |
93 | | ffun 6294 |
. . . . . . . . . 10
⊢ (𝐹:𝑋⟶ℝ → Fun 𝐹) |
94 | 9, 10, 93 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → Fun 𝐹) |
95 | | fdm 6299 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋⟶ℝ → dom 𝐹 = 𝑋) |
96 | 9, 10, 95 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝑋) |
97 | 25, 96 | sseqtr4d 3861 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ dom 𝐹) |
98 | | funfvima2 6765 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ dom 𝐹) → (𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) → (𝐹‘𝐶) ∈ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
99 | 94, 97, 98 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) → (𝐹‘𝐶) ∈ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
100 | 92, 99 | mpd 15 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
101 | 47 | cnfldtopon 22994 |
. . . . . . . . 9
⊢ 𝐽 ∈
(TopOn‘ℂ) |
102 | | resttopon 21373 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℂ) → (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (TopOn‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
103 | 101, 70, 102 | sylancr 581 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (TopOn‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
104 | | toponuni 21126 |
. . . . . . . 8
⊢ ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (TopOn‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
105 | 103, 104 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
106 | 100, 105 | eleqtrd 2861 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐶) ∈ ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
107 | | eqid 2778 |
. . . . . . 7
⊢ ∪ (𝐽
↾t (𝐹
“ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
108 | 107 | cncnpi 21490 |
. . . . . 6
⊢ ((◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) Cn 𝑀) ∧ (𝐹‘𝐶) ∈ ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶))) |
109 | 85, 106, 108 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶))) |
110 | 36, 109 | eqeltrrd 2860 |
. . . 4
⊢ (𝜑 → (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶))) |
111 | | dvcnvre.n |
. . . . . . . 8
⊢ 𝑁 = (𝐽 ↾t 𝑌) |
112 | 111 | oveq1i 6932 |
. . . . . . 7
⊢ (𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = ((𝐽 ↾t 𝑌) ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
113 | | ssexg 5041 |
. . . . . . . . 9
⊢ ((𝑌 ⊆ ℝ ∧ ℝ
∈ V) → 𝑌 ∈
V) |
114 | 13, 54, 113 | sylancl 580 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ V) |
115 | | restabs 21377 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ 𝑌 ∧ 𝑌 ∈ V) → ((𝐽 ↾t 𝑌) ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
116 | 52, 15, 114, 115 | syl3anc 1439 |
. . . . . . 7
⊢ (𝜑 → ((𝐽 ↾t 𝑌) ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
117 | 112, 116 | syl5eq 2826 |
. . . . . 6
⊢ (𝜑 → (𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
118 | 117 | oveq1d 6937 |
. . . . 5
⊢ (𝜑 → ((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀) = ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)) |
119 | 118 | fveq1d 6448 |
. . . 4
⊢ (𝜑 → (((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶)) = (((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶))) |
120 | 110, 119 | eleqtrrd 2862 |
. . 3
⊢ (𝜑 → (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶))) |
121 | 13, 39 | syl6ss 3833 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ⊆ ℂ) |
122 | | resttopon 21373 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝑌 ⊆ ℂ)
→ (𝐽
↾t 𝑌)
∈ (TopOn‘𝑌)) |
123 | 101, 121,
122 | sylancr 581 |
. . . . . 6
⊢ (𝜑 → (𝐽 ↾t 𝑌) ∈ (TopOn‘𝑌)) |
124 | 111, 123 | syl5eqel 2863 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (TopOn‘𝑌)) |
125 | | topontop 21125 |
. . . . 5
⊢ (𝑁 ∈ (TopOn‘𝑌) → 𝑁 ∈ Top) |
126 | 124, 125 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ Top) |
127 | | toponuni 21126 |
. . . . . 6
⊢ (𝑁 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝑁) |
128 | 124, 127 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑌 = ∪ 𝑁) |
129 | 15, 128 | sseqtrd 3860 |
. . . 4
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ∪
𝑁) |
130 | 15, 13 | sstrd 3831 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℝ) |
131 | | difssd 3961 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ ∖ 𝑌) ⊆
ℝ) |
132 | 130, 131 | unssd 4012 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)) ⊆ ℝ) |
133 | | ssun1 3999 |
. . . . . . . . 9
⊢ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)) |
134 | 133 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) |
135 | 18 | ntrss 21267 |
. . . . . . . 8
⊢ ((𝑇 ∈ Top ∧ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)) ⊆ ℝ ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) → ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ⊆ ((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)))) |
136 | 4, 132, 134, 135 | syl3anc 1439 |
. . . . . . 7
⊢ (𝜑 → ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ⊆ ((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)))) |
137 | 136, 29 | sseldd 3822 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)))) |
138 | | f1of 6391 |
. . . . . . . 8
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋⟶𝑌) |
139 | 5, 138 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
140 | 139, 23 | ffvelrnd 6624 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝑌) |
141 | 137, 140 | elind 4021 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐶) ∈ (((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) ∩ 𝑌)) |
142 | | eqid 2778 |
. . . . . . . 8
⊢ (𝑇 ↾t 𝑌) = (𝑇 ↾t 𝑌) |
143 | 18, 142 | restntr 21394 |
. . . . . . 7
⊢ ((𝑇 ∈ Top ∧ 𝑌 ⊆ ℝ ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ 𝑌) → ((int‘(𝑇 ↾t 𝑌))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) ∩ 𝑌)) |
144 | 4, 13, 15, 143 | syl3anc 1439 |
. . . . . 6
⊢ (𝜑 → ((int‘(𝑇 ↾t 𝑌))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) ∩ 𝑌)) |
145 | | restabs 21377 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ ℝ ∧ ℝ
∈ V) → ((𝐽
↾t ℝ) ↾t 𝑌) = (𝐽 ↾t 𝑌)) |
146 | 52, 13, 55, 145 | syl3anc 1439 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐽 ↾t ℝ)
↾t 𝑌) =
(𝐽 ↾t
𝑌)) |
147 | 49 | oveq1i 6932 |
. . . . . . . . 9
⊢ (𝑇 ↾t 𝑌) = ((𝐽 ↾t ℝ)
↾t 𝑌) |
148 | 146, 147,
111 | 3eqtr4g 2839 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ↾t 𝑌) = 𝑁) |
149 | 148 | fveq2d 6450 |
. . . . . . 7
⊢ (𝜑 → (int‘(𝑇 ↾t 𝑌)) = (int‘𝑁)) |
150 | 149 | fveq1d 6448 |
. . . . . 6
⊢ (𝜑 → ((int‘(𝑇 ↾t 𝑌))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = ((int‘𝑁)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
151 | 144, 150 | eqtr3d 2816 |
. . . . 5
⊢ (𝜑 → (((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) ∩ 𝑌) = ((int‘𝑁)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
152 | 141, 151 | eleqtrd 2861 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝑁)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
153 | 128 | feq2d 6277 |
. . . . . 6
⊢ (𝜑 → (◡𝐹:𝑌⟶𝑋 ↔ ◡𝐹:∪ 𝑁⟶𝑋)) |
154 | 33, 153 | mpbid 224 |
. . . . 5
⊢ (𝜑 → ◡𝐹:∪ 𝑁⟶𝑋) |
155 | | resttopon 21373 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝑋 ⊆ ℂ)
→ (𝐽
↾t 𝑋)
∈ (TopOn‘𝑋)) |
156 | 101, 40, 155 | sylancr 581 |
. . . . . . 7
⊢ (𝜑 → (𝐽 ↾t 𝑋) ∈ (TopOn‘𝑋)) |
157 | 82, 156 | syl5eqel 2863 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑋)) |
158 | | toponuni 21126 |
. . . . . 6
⊢ (𝑀 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑀) |
159 | | feq3 6274 |
. . . . . 6
⊢ (𝑋 = ∪
𝑀 → (◡𝐹:∪ 𝑁⟶𝑋 ↔ ◡𝐹:∪ 𝑁⟶∪ 𝑀)) |
160 | 157, 158,
159 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (◡𝐹:∪ 𝑁⟶𝑋 ↔ ◡𝐹:∪ 𝑁⟶∪ 𝑀)) |
161 | 154, 160 | mpbid 224 |
. . . 4
⊢ (𝜑 → ◡𝐹:∪ 𝑁⟶∪ 𝑀) |
162 | | eqid 2778 |
. . . . 5
⊢ ∪ 𝑁 =
∪ 𝑁 |
163 | | eqid 2778 |
. . . . 5
⊢ ∪ 𝑀 =
∪ 𝑀 |
164 | 162, 163 | cnprest 21501 |
. . . 4
⊢ (((𝑁 ∈ Top ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ∪
𝑁) ∧ ((𝐹‘𝐶) ∈ ((int‘𝑁)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∧ ◡𝐹:∪ 𝑁⟶∪ 𝑀))
→ (◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶)) ↔ (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶)))) |
165 | 126, 129,
152, 161, 164 | syl22anc 829 |
. . 3
⊢ (𝜑 → (◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶)) ↔ (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶)))) |
166 | 120, 165 | mpbird 249 |
. 2
⊢ (𝜑 → ◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶))) |
167 | 30, 166 | jca 507 |
1
⊢ (𝜑 → ((𝐹‘𝐶) ∈ ((int‘𝑇)‘𝑌) ∧ ◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶)))) |