Metamath Proof Explorer

Theorem dvcnvre

Description: The derivative rule for inverse functions. If F is a continuous and differentiable bijective function from X to Y which never has derivative 0 , then ` ``' F is also differentiable, and its derivative is the reciprocal of the derivative of F ` . (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses dvcnvre.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 –cn→ ℝ ) )
dvcnvre.d ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = 𝑋 )
dvcnvre.z ⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐹 ) )
dvcnvre.1 ⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
Assertion dvcnvre ( 𝜑 → ( ℝ D ◡ 𝐹 ) = ( 𝑥 ∈ 𝑌 ↦ ( 1 / ( ( ℝ D 𝐹 ) ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dvcnvre.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 –cn→ ℝ ) )
2 dvcnvre.d ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = 𝑋 )
3 dvcnvre.z ⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐹 ) )
4 dvcnvre.1 ⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
5 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
6 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
7 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
8 7 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
9 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
10 f1ofo ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –onto→ 𝑌 )
11 forn ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ran 𝐹 = 𝑌 )
12 4 10 11 3syl ⊢ ( 𝜑 → ran 𝐹 = 𝑌 )
13 cncff ⊢ ( 𝐹 ∈ ( 𝑋 –cn→ ℝ ) → 𝐹 : 𝑋 ⟶ ℝ )
14 frn ⊢ ( 𝐹 : 𝑋 ⟶ ℝ → ran 𝐹 ⊆ ℝ )
15 1 13 14 3syl ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
16 12 15 eqsstrrd ⊢ ( 𝜑 → 𝑌 ⊆ ℝ )
17 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
18 17 ntrss2 ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝑌 ⊆ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) ⊆ 𝑌 )
19 9 16 18 sylancr ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) ⊆ 𝑌 )
20 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
21 4 20 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) = 𝑥 )
22 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
23 22 rexmet ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
24 dvbsss ⊢ dom ( ℝ D 𝐹 ) ⊆ ℝ
25 24 a1i ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) ⊆ ℝ )
26 2 25 eqsstrrd ⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
27 17 ntrss2 ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝑋 ⊆ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) ⊆ 𝑋 )
28 9 26 27 sylancr ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) ⊆ 𝑋 )
29 ax-resscn ⊢ ℝ ⊆ ℂ
30 29 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
31 1 13 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
32 fss ⊢ ( ( 𝐹 : 𝑋 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : 𝑋 ⟶ ℂ )
33 31 29 32 sylancl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
34 30 33 26 6 5 dvbssntr ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) )
35 2 34 eqsstrrd ⊢ ( 𝜑 → 𝑋 ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) )
36 28 35 eqssd ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) = 𝑋 )
37 17 isopn3 ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝑋 ⊆ ℝ ) → ( 𝑋 ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) = 𝑋 ) )
38 9 26 37 sylancr ⊢ ( 𝜑 → ( 𝑋 ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑋 ) = 𝑋 ) )
39 36 38 mpbird ⊢ ( 𝜑 → 𝑋 ∈ ( topGen ‘ ran (,) ) )
40 f1ocnv ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
41 f1of ⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
42 4 40 41 3syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
43 42 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 )
44 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
45 22 44 tgioo ⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
46 45 mopni2 ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ 𝑋 ∈ ( topGen ‘ ran (,) ) ∧ ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 ) → ∃ 𝑟 ∈ ℝ+ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 )
47 23 39 43 46 mp3an2ani ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ∃ 𝑟 ∈ ℝ+ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 )
48 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → 𝐹 ∈ ( 𝑋 –cn→ ℝ ) )
49 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → dom ( ℝ D 𝐹 ) = 𝑋 )
50 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ¬ 0 ∈ ran ( ℝ D 𝐹 ) )
51 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
52 43 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ 𝑋 )
53 rphalfcl ⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ+ )
54 53 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( 𝑟 / 2 ) ∈ ℝ+ )
55 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → 𝑋 ⊆ ℝ )
56 55 52 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ ℝ )
57 54 rpred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( 𝑟 / 2 ) ∈ ℝ )
58 56 57 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) ∈ ℝ )
59 56 57 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ∈ ℝ )
60 elicc2 ⊢ ( ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) ∈ ℝ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ∈ ℝ ) → ( 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) ≤ 𝑦 ∧ 𝑦 ≤ ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) )
61 58 59 60 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) ≤ 𝑦 ∧ 𝑦 ≤ ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) )
62 61 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( 𝑦 ∈ ℝ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) ≤ 𝑦 ∧ 𝑦 ≤ ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) )
63 62 simp1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → 𝑦 ∈ ℝ )
64 56 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ ℝ )
65 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → 𝑟 ∈ ℝ+ )
66 65 rpred ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → 𝑟 ∈ ℝ )
67 64 66 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) ∈ ℝ )
68 58 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) ∈ ℝ )
69 65 53 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( 𝑟 / 2 ) ∈ ℝ+ )
70 69 rpred ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( 𝑟 / 2 ) ∈ ℝ )
71 rphalflt ⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) < 𝑟 )
72 65 71 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( 𝑟 / 2 ) < 𝑟 )
73 70 66 64 72 ltsub2dd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) < ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) )
74 62 simp2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) ≤ 𝑦 )
75 67 68 63 73 74 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) < 𝑦 )
76 59 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ∈ ℝ )
77 64 66 readdcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) ∈ ℝ )
78 62 simp3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → 𝑦 ≤ ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) )
79 70 66 64 72 ltadd2dd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) < ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) )
80 63 76 77 78 79 lelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → 𝑦 < ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) )
81 67 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) ∈ ℝ* )
82 77 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) ∈ ℝ* )
83 elioo2 ⊢ ( ( ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) ∈ ℝ* ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) ∈ ℝ* ) → ( 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) (,) ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) < 𝑦 ∧ 𝑦 < ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) ) ) )
84 81 82 83 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → ( 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) (,) ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) < 𝑦 ∧ 𝑦 < ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) ) ) )
85 63 75 80 84 mpbir3and ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) ∧ 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ) → 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) (,) ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) ) )
86 85 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) → 𝑦 ∈ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) (,) ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) ) ) )
87 86 ssrdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ⊆ ( ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) (,) ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) ) )
88 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
89 88 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → 𝑟 ∈ ℝ )
90 22 bl2ioo ⊢ ( ( ( ◡ 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) (,) ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) ) )
91 56 89 90 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( ( ◡ 𝐹 ‘ 𝑥 ) − 𝑟 ) (,) ( ( ◡ 𝐹 ‘ 𝑥 ) + 𝑟 ) ) )
92 87 91 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ⊆ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) )
93 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 )
94 92 93 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑥 ) − ( 𝑟 / 2 ) ) [,] ( ( ◡ 𝐹 ‘ 𝑥 ) + ( 𝑟 / 2 ) ) ) ⊆ 𝑋 )
95 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
96 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 )
97 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 )
98 48 49 50 51 52 54 94 95 5 96 97 dvcnvrelem2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( ◡ 𝐹 ‘ 𝑥 ) ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝑋 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) ∧ ◡ 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) CnP ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) ‘ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) ) )
99 47 98 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) ∧ ◡ 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) CnP ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) ‘ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) ) )
100 99 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) )
101 21 100 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) )
102 19 101 eqelssd ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) = 𝑌 )
103 17 isopn3 ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝑌 ⊆ ℝ ) → ( 𝑌 ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) = 𝑌 ) )
104 9 16 103 sylancr ⊢ ( 𝜑 → ( 𝑌 ∈ ( topGen ‘ ran (,) ) ↔ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝑌 ) = 𝑌 ) )
105 102 104 mpbird ⊢ ( 𝜑 → 𝑌 ∈ ( topGen ‘ ran (,) ) )
106 99 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ◡ 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) CnP ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) ‘ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) )
107 21 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) CnP ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) ‘ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) CnP ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) ‘ 𝑥 ) )
108 106 107 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ◡ 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) CnP ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) ‘ 𝑥 ) )
109 108 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑌 ◡ 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) CnP ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) ‘ 𝑥 ) )
110 5 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
111 16 29 sstrdi ⊢ ( 𝜑 → 𝑌 ⊆ ℂ )
112 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑌 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
113 110 111 112 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
114 26 29 sstrdi ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
115 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑋 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
116 110 114 115 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
117 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) ∧ ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) ) → ( ◡ 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) ↔ ( ◡ 𝐹 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑌 ◡ 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) CnP ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) ‘ 𝑥 ) ) ) )
118 113 116 117 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) ↔ ( ◡ 𝐹 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑌 ◡ 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) CnP ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) ‘ 𝑥 ) ) ) )
119 42 109 118 mpbir2and ⊢ ( 𝜑 → ◡ 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) )
120 5 97 96 cncfcn ⊢ ( ( 𝑌 ⊆ ℂ ∧ 𝑋 ⊆ ℂ ) → ( 𝑌 –cn→ 𝑋 ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) )
121 111 114 120 syl2anc ⊢ ( 𝜑 → ( 𝑌 –cn→ 𝑋 ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑌 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝑋 ) ) )
122 119 121 eleqtrrd ⊢ ( 𝜑 → ◡ 𝐹 ∈ ( 𝑌 –cn→ 𝑋 ) )
123 5 6 8 105 4 122 2 3 dvcnv ⊢ ( 𝜑 → ( ℝ D ◡ 𝐹 ) = ( 𝑥 ∈ 𝑌 ↦ ( 1 / ( ( ℝ D 𝐹 ) ‘ ( ◡ 𝐹 ‘ 𝑥 ) ) ) ) )