Proof of Theorem dvcnvrelem2
| Step | Hyp | Ref
| Expression |
| 1 | | dvcnvre.t |
. . . . 5
⊢ 𝑇 = (topGen‘ran
(,)) |
| 2 | | retop 24782 |
. . . . 5
⊢
(topGen‘ran (,)) ∈ Top |
| 3 | 1, 2 | eqeltri 2837 |
. . . 4
⊢ 𝑇 ∈ Top |
| 4 | | dvcnvre.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑋–1-1-onto→𝑌) |
| 5 | | f1ofo 6855 |
. . . . . 6
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–onto→𝑌) |
| 6 | | forn 6823 |
. . . . . 6
⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌) |
| 7 | 4, 5, 6 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ran 𝐹 = 𝑌) |
| 8 | | dvcnvre.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑋–cn→ℝ)) |
| 9 | | cncff 24919 |
. . . . . 6
⊢ (𝐹 ∈ (𝑋–cn→ℝ) → 𝐹:𝑋⟶ℝ) |
| 10 | | frn 6743 |
. . . . . 6
⊢ (𝐹:𝑋⟶ℝ → ran 𝐹 ⊆ ℝ) |
| 11 | 8, 9, 10 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
| 12 | 7, 11 | eqsstrrd 4019 |
. . . 4
⊢ (𝜑 → 𝑌 ⊆ ℝ) |
| 13 | | imassrn 6089 |
. . . . 5
⊢ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ran 𝐹 |
| 14 | 13, 7 | sseqtrid 4026 |
. . . 4
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ 𝑌) |
| 15 | | uniretop 24783 |
. . . . . 6
⊢ ℝ =
∪ (topGen‘ran (,)) |
| 16 | 1 | unieqi 4919 |
. . . . . 6
⊢ ∪ 𝑇 =
∪ (topGen‘ran (,)) |
| 17 | 15, 16 | eqtr4i 2768 |
. . . . 5
⊢ ℝ =
∪ 𝑇 |
| 18 | 17 | ntrss 23063 |
. . . 4
⊢ ((𝑇 ∈ Top ∧ 𝑌 ⊆ ℝ ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ 𝑌) → ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ⊆ ((int‘𝑇)‘𝑌)) |
| 19 | 3, 12, 14, 18 | mp3an2i 1468 |
. . 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 26056 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘(topGen‘ran
(,)))‘(𝐹 “
((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 26 | 1 | fveq2i 6909 |
. . . . 5
⊢
(int‘𝑇) =
(int‘(topGen‘ran (,))) |
| 27 | 26 | fveq1i 6907 |
. . . 4
⊢
((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = ((int‘(topGen‘ran
(,)))‘(𝐹 “
((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
| 28 | 25, 27 | eleqtrrdi 2852 |
. . 3
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 29 | 19, 28 | sseldd 3984 |
. 2
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝑇)‘𝑌)) |
| 30 | | f1ocnv 6860 |
. . . . . . 7
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌–1-1-onto→𝑋) |
| 31 | | f1of 6848 |
. . . . . . 7
⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → ◡𝐹:𝑌⟶𝑋) |
| 32 | 4, 30, 31 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ◡𝐹:𝑌⟶𝑋) |
| 33 | | ffun 6739 |
. . . . . 6
⊢ (◡𝐹:𝑌⟶𝑋 → Fun ◡𝐹) |
| 34 | | funcnvres 6644 |
. . . . . 6
⊢ (Fun
◡𝐹 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 35 | 32, 33, 34 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 36 | | dvbsss 25937 |
. . . . . . . . . . 11
⊢ dom
(ℝ D 𝐹) ⊆
ℝ |
| 37 | 20, 36 | eqsstrrdi 4029 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆ ℝ) |
| 38 | | ax-resscn 11212 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
| 39 | 37, 38 | sstrdi 3996 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
| 40 | | cncfss 24925 |
. . . . . . . . 9
⊢ ((((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋 ∧ 𝑋 ⊆ ℂ) → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋)) |
| 41 | 24, 39, 40 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋)) |
| 42 | | f1of1 6847 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–1-1→𝑌) |
| 43 | 4, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑋–1-1→𝑌) |
| 44 | | f1ores 6862 |
. . . . . . . . . 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 24824 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) = (𝐽 ↾t
ℝ) |
| 48 | 1, 47 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ 𝑇 = (𝐽 ↾t
ℝ) |
| 49 | 48 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = ((𝐽 ↾t ℝ)
↾t ((𝐶
− 𝑅)[,](𝐶 + 𝑅))) |
| 50 | 46 | cnfldtop 24804 |
. . . . . . . . . . . . 13
⊢ 𝐽 ∈ Top |
| 51 | 24, 37 | sstrd 3994 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ ℝ) |
| 52 | | reex 11246 |
. . . . . . . . . . . . . 14
⊢ ℝ
∈ V |
| 53 | 52 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ∈
V) |
| 54 | | restabs 23173 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ ℝ ∧ ℝ ∈ V)
→ ((𝐽
↾t ℝ) ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
| 55 | 50, 51, 53, 54 | mp3an2i 1468 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐽 ↾t ℝ)
↾t ((𝐶
− 𝑅)[,](𝐶 + 𝑅))) = (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
| 56 | 49, 55 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
| 57 | 37, 22 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 58 | 23 | rpred 13077 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ ℝ) |
| 59 | 57, 58 | resubcld 11691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 − 𝑅) ∈ ℝ) |
| 60 | 57, 58 | readdcld 11290 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 + 𝑅) ∈ ℝ) |
| 61 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) |
| 62 | 1, 61 | icccmp 24847 |
. . . . . . . . . . . 12
⊢ (((𝐶 − 𝑅) ∈ ℝ ∧ (𝐶 + 𝑅) ∈ ℝ) → (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ Comp) |
| 63 | 59, 60, 62 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ Comp) |
| 64 | 56, 63 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ Comp) |
| 65 | | f1of 6848 |
. . . . . . . . . . . 12
⊢ ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))⟶(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
| 66 | 45, 65 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))⟶(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
| 67 | 11, 38 | sstrdi 3996 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝐹 ⊆ ℂ) |
| 68 | 13, 67 | sstrid 3995 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℂ) |
| 69 | | rescncf 24923 |
. . . . . . . . . . . . 13
⊢ (((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋 → (𝐹 ∈ (𝑋–cn→ℝ) → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→ℝ))) |
| 70 | 24, 8, 69 | sylc 65 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→ℝ)) |
| 71 | | cncfcdm 24924 |
. . . . . . . . . . . 12
⊢ (((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℂ ∧ (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→ℝ)) → ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ↔ (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))⟶(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 72 | 68, 70, 71 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ↔ (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))⟶(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 73 | 66, 72 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 74 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = (𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) |
| 75 | 46, 74 | cncfcnvcn 24952 |
. . . . . . . . . 10
⊢ (((𝐽 ↾t ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ Comp ∧ (𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶 − 𝑅)[,](𝐶 + 𝑅))–cn→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) → ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ↔ ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 76 | 64, 73, 75 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))):((𝐶 − 𝑅)[,](𝐶 + 𝑅))–1-1-onto→(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ↔ ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 77 | 45, 76 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
| 78 | 41, 77 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → ◡(𝐹 ↾ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∈ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))–cn→𝑋)) |
| 79 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
| 80 | | dvcnvre.m |
. . . . . . . . 9
⊢ 𝑀 = (𝐽 ↾t 𝑋) |
| 81 | 46, 79, 80 | cncfcn 24936 |
. . . . . . . 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 13109 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 − 𝑅) < 𝐶) |
| 85 | 59, 57, 84 | ltled 11409 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 − 𝑅) ≤ 𝐶) |
| 86 | 57, 23 | ltaddrpd 13110 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 < (𝐶 + 𝑅)) |
| 87 | 57, 60, 86 | ltled 11409 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ≤ (𝐶 + 𝑅)) |
| 88 | | elicc2 13452 |
. . . . . . . . . 10
⊢ (((𝐶 − 𝑅) ∈ ℝ ∧ (𝐶 + 𝑅) ∈ ℝ) → (𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ↔ (𝐶 ∈ ℝ ∧ (𝐶 − 𝑅) ≤ 𝐶 ∧ 𝐶 ≤ (𝐶 + 𝑅)))) |
| 89 | 59, 60, 88 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ↔ (𝐶 ∈ ℝ ∧ (𝐶 − 𝑅) ≤ 𝐶 ∧ 𝐶 ≤ (𝐶 + 𝑅)))) |
| 90 | 57, 85, 87, 89 | mpbir3and 1343 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) |
| 91 | | ffun 6739 |
. . . . . . . . . 10
⊢ (𝐹:𝑋⟶ℝ → Fun 𝐹) |
| 92 | 8, 9, 91 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → Fun 𝐹) |
| 93 | | fdm 6745 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋⟶ℝ → dom 𝐹 = 𝑋) |
| 94 | 8, 9, 93 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝑋) |
| 95 | 24, 94 | sseqtrrd 4021 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ dom 𝐹) |
| 96 | | funfvima2 7251 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) ⊆ dom 𝐹) → (𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) → (𝐹‘𝐶) ∈ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 97 | 92, 95, 96 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)) → (𝐹‘𝐶) ∈ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 98 | 90, 97 | mpd 15 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐶) ∈ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
| 99 | 46 | cnfldtopon 24803 |
. . . . . . . . 9
⊢ 𝐽 ∈
(TopOn‘ℂ) |
| 100 | | resttopon 23169 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℂ) → (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (TopOn‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 101 | 99, 68, 100 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (TopOn‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 102 | | toponuni 22920 |
. . . . . . . 8
⊢ ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (TopOn‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 103 | 101, 102 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) = ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 104 | 98, 103 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐶) ∈ ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 105 | | eqid 2737 |
. . . . . . 7
⊢ ∪ (𝐽
↾t (𝐹
“ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = ∪ (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
| 106 | 105 | cncnpi 23286 |
. . . . . 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 7441 |
. . . . . . 7
⊢ (𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = ((𝐽 ↾t 𝑌) ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) |
| 111 | | ssexg 5323 |
. . . . . . . . 9
⊢ ((𝑌 ⊆ ℝ ∧ ℝ
∈ V) → 𝑌 ∈
V) |
| 112 | 12, 52, 111 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ V) |
| 113 | | restabs 23173 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ 𝑌 ∧ 𝑌 ∈ V) → ((𝐽 ↾t 𝑌) ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 114 | 50, 14, 112, 113 | mp3an2i 1468 |
. . . . . . 7
⊢ (𝜑 → ((𝐽 ↾t 𝑌) ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 115 | 110, 114 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → (𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 116 | 115 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → ((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀) = ((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)) |
| 117 | 116 | fveq1d 6908 |
. . . 4
⊢ (𝜑 → (((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶)) = (((𝐽 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶))) |
| 118 | 108, 117 | eleqtrrd 2844 |
. . 3
⊢ (𝜑 → (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶))) |
| 119 | 12, 38 | sstrdi 3996 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ⊆ ℂ) |
| 120 | | resttopon 23169 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝑌 ⊆ ℂ)
→ (𝐽
↾t 𝑌)
∈ (TopOn‘𝑌)) |
| 121 | 99, 119, 120 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (𝐽 ↾t 𝑌) ∈ (TopOn‘𝑌)) |
| 122 | 109, 121 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (TopOn‘𝑌)) |
| 123 | | topontop 22919 |
. . . . 5
⊢ (𝑁 ∈ (TopOn‘𝑌) → 𝑁 ∈ Top) |
| 124 | 122, 123 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ Top) |
| 125 | | toponuni 22920 |
. . . . . 6
⊢ (𝑁 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝑁) |
| 126 | 122, 125 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑌 = ∪ 𝑁) |
| 127 | 14, 126 | sseqtrd 4020 |
. . . 4
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ∪
𝑁) |
| 128 | 14, 12 | sstrd 3994 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ℝ) |
| 129 | | difssd 4137 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ ∖ 𝑌) ⊆
ℝ) |
| 130 | 128, 129 | unssd 4192 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)) ⊆ ℝ) |
| 131 | | ssun1 4178 |
. . . . . . . . 9
⊢ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)) |
| 132 | 131 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) |
| 133 | 17 | ntrss 23063 |
. . . . . . . 8
⊢ ((𝑇 ∈ Top ∧ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)) ⊆ ℝ ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) → ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ⊆ ((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)))) |
| 134 | 3, 130, 132, 133 | mp3an2i 1468 |
. . . . . . 7
⊢ (𝜑 → ((int‘𝑇)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ⊆ ((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)))) |
| 135 | 134, 28 | sseldd 3984 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌)))) |
| 136 | | f1of 6848 |
. . . . . . . 8
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋⟶𝑌) |
| 137 | 4, 136 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
| 138 | 137, 22 | ffvelcdmd 7105 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝑌) |
| 139 | 135, 138 | elind 4200 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐶) ∈ (((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) ∩ 𝑌)) |
| 140 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑇 ↾t 𝑌) = (𝑇 ↾t 𝑌) |
| 141 | 17, 140 | restntr 23190 |
. . . . . . 7
⊢ ((𝑇 ∈ Top ∧ 𝑌 ⊆ ℝ ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ 𝑌) → ((int‘(𝑇 ↾t 𝑌))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) ∩ 𝑌)) |
| 142 | 3, 12, 14, 141 | mp3an2i 1468 |
. . . . . 6
⊢ (𝜑 → ((int‘(𝑇 ↾t 𝑌))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = (((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) ∩ 𝑌)) |
| 143 | | restabs 23173 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ ℝ ∧ ℝ
∈ V) → ((𝐽
↾t ℝ) ↾t 𝑌) = (𝐽 ↾t 𝑌)) |
| 144 | 50, 12, 53, 143 | mp3an2i 1468 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐽 ↾t ℝ)
↾t 𝑌) =
(𝐽 ↾t
𝑌)) |
| 145 | 48 | oveq1i 7441 |
. . . . . . . . 9
⊢ (𝑇 ↾t 𝑌) = ((𝐽 ↾t ℝ)
↾t 𝑌) |
| 146 | 144, 145,
109 | 3eqtr4g 2802 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ↾t 𝑌) = 𝑁) |
| 147 | 146 | fveq2d 6910 |
. . . . . . 7
⊢ (𝜑 → (int‘(𝑇 ↾t 𝑌)) = (int‘𝑁)) |
| 148 | 147 | fveq1d 6908 |
. . . . . 6
⊢ (𝜑 → ((int‘(𝑇 ↾t 𝑌))‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) = ((int‘𝑁)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 149 | 142, 148 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → (((int‘𝑇)‘((𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ∪ (ℝ ∖ 𝑌))) ∩ 𝑌) = ((int‘𝑁)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 150 | 139, 149 | eleqtrd 2843 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐶) ∈ ((int‘𝑁)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))))) |
| 151 | 126 | feq2d 6722 |
. . . . . 6
⊢ (𝜑 → (◡𝐹:𝑌⟶𝑋 ↔ ◡𝐹:∪ 𝑁⟶𝑋)) |
| 152 | 32, 151 | mpbid 232 |
. . . . 5
⊢ (𝜑 → ◡𝐹:∪ 𝑁⟶𝑋) |
| 153 | | resttopon 23169 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝑋 ⊆ ℂ)
→ (𝐽
↾t 𝑋)
∈ (TopOn‘𝑋)) |
| 154 | 99, 39, 153 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (𝐽 ↾t 𝑋) ∈ (TopOn‘𝑋)) |
| 155 | 80, 154 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑋)) |
| 156 | | toponuni 22920 |
. . . . . 6
⊢ (𝑀 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑀) |
| 157 | | feq3 6718 |
. . . . . 6
⊢ (𝑋 = ∪
𝑀 → (◡𝐹:∪ 𝑁⟶𝑋 ↔ ◡𝐹:∪ 𝑁⟶∪ 𝑀)) |
| 158 | 155, 156,
157 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (◡𝐹:∪ 𝑁⟶𝑋 ↔ ◡𝐹:∪ 𝑁⟶∪ 𝑀)) |
| 159 | 152, 158 | mpbid 232 |
. . . 4
⊢ (𝜑 → ◡𝐹:∪ 𝑁⟶∪ 𝑀) |
| 160 | | eqid 2737 |
. . . . 5
⊢ ∪ 𝑁 =
∪ 𝑁 |
| 161 | | eqid 2737 |
. . . . 5
⊢ ∪ 𝑀 =
∪ 𝑀 |
| 162 | 160, 161 | cnprest 23297 |
. . . 4
⊢ (((𝑁 ∈ Top ∧ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅))) ⊆ ∪
𝑁) ∧ ((𝐹‘𝐶) ∈ ((int‘𝑁)‘(𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∧ ◡𝐹:∪ 𝑁⟶∪ 𝑀))
→ (◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶)) ↔ (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶)))) |
| 163 | 124, 127,
150, 159, 162 | syl22anc 839 |
. . 3
⊢ (𝜑 → (◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶)) ↔ (◡𝐹 ↾ (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) ∈ (((𝑁 ↾t (𝐹 “ ((𝐶 − 𝑅)[,](𝐶 + 𝑅)))) CnP 𝑀)‘(𝐹‘𝐶)))) |
| 164 | 118, 163 | mpbird 257 |
. 2
⊢ (𝜑 → ◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶))) |
| 165 | 29, 164 | jca 511 |
1
⊢ (𝜑 → ((𝐹‘𝐶) ∈ ((int‘𝑇)‘𝑌) ∧ ◡𝐹 ∈ ((𝑁 CnP 𝑀)‘(𝐹‘𝐶)))) |