Metamath Proof Explorer

Theorem dvcnvrelem2

Description: Lemma for dvcnvre . (Contributed by Mario Carneiro, 19-Feb-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypotheses dvcnvre.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 –cn→ ℝ ) )
dvcnvre.d ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = 𝑋 )
dvcnvre.z ⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐹 ) )
dvcnvre.1 ⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
dvcnvre.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
dvcnvre.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
dvcnvre.s ⊢ ( 𝜑 → ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ 𝑋 )
dvcnvre.t ⊢ 𝑇 = ( topGen ‘ ran (,) )
dvcnvre.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
dvcnvre.m ⊢ 𝑀 = ( 𝐽 ↾t 𝑋 )
dvcnvre.n ⊢ 𝑁 = ( 𝐽 ↾t 𝑌 )
Assertion dvcnvrelem2 ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ 𝑇 ) ‘ 𝑌 ) ∧ ◡ 𝐹 ∈ ( ( 𝑁 CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) ) )

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 dvcnvre.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
6 dvcnvre.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
7 dvcnvre.s ⊢ ( 𝜑 → ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ 𝑋 )
8 dvcnvre.t ⊢ 𝑇 = ( topGen ‘ ran (,) )
9 dvcnvre.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
10 dvcnvre.m ⊢ 𝑀 = ( 𝐽 ↾t 𝑋 )
11 dvcnvre.n ⊢ 𝑁 = ( 𝐽 ↾t 𝑌 )
12 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
13 8 12 eqeltri ⊢ 𝑇 ∈ Top
14 f1ofo ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –onto→ 𝑌 )
15 forn ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ran 𝐹 = 𝑌 )
16 4 14 15 3syl ⊢ ( 𝜑 → ran 𝐹 = 𝑌 )
17 cncff ⊢ ( 𝐹 ∈ ( 𝑋 –cn→ ℝ ) → 𝐹 : 𝑋 ⟶ ℝ )
18 frn ⊢ ( 𝐹 : 𝑋 ⟶ ℝ → ran 𝐹 ⊆ ℝ )
19 1 17 18 3syl ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
20 16 19 eqsstrrd ⊢ ( 𝜑 → 𝑌 ⊆ ℝ )
21 imassrn ⊢ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ran 𝐹
22 21 16 sseqtrid ⊢ ( 𝜑 → ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ 𝑌 )
23 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
24 8 unieqi ⊢ ∪ 𝑇 = ∪ ( topGen ‘ ran (,) )
25 23 24 eqtr4i ⊢ ℝ = ∪ 𝑇
26 25 ntrss ⊢ ( ( 𝑇 ∈ Top ∧ 𝑌 ⊆ ℝ ∧ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ 𝑌 ) → ( ( int ‘ 𝑇 ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ⊆ ( ( int ‘ 𝑇 ) ‘ 𝑌 ) )
27 13 20 22 26 mp3an2i ⊢ ( 𝜑 → ( ( int ‘ 𝑇 ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ⊆ ( ( int ‘ 𝑇 ) ‘ 𝑌 ) )
28 1 2 3 4 5 6 7 dvcnvrelem1 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
29 8 fveq2i ⊢ ( int ‘ 𝑇 ) = ( int ‘ ( topGen ‘ ran (,) ) )
30 29 fveq1i ⊢ ( ( int ‘ 𝑇 ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
31 28 30 eleqtrrdi ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
32 27 31 sseldd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ 𝑇 ) ‘ 𝑌 ) )
33 f1ocnv ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
34 f1of ⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
35 4 33 34 3syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
36 ffun ⊢ ( ◡ 𝐹 : 𝑌 ⟶ 𝑋 → Fun ◡ 𝐹 )
37 funcnvres ⊢ ( Fun ◡ 𝐹 → ◡ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( ◡ 𝐹 ↾ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
38 35 36 37 3syl ⊢ ( 𝜑 → ◡ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( ◡ 𝐹 ↾ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
39 dvbsss ⊢ dom ( ℝ D 𝐹 ) ⊆ ℝ
40 2 39 eqsstrrdi ⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
41 ax-resscn ⊢ ℝ ⊆ ℂ
42 40 41 sstrdi ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
43 cncfss ⊢ ( ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ 𝑋 ∧ 𝑋 ⊆ ℂ ) → ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) –cn→ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) –cn→ 𝑋 ) )
44 7 42 43 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) –cn→ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) –cn→ 𝑋 ) )
45 f1of1 ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –1-1→ 𝑌 )
46 4 45 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1→ 𝑌 )
47 f1ores ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ 𝑋 ) → ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) : ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –1-1-onto→ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
48 46 7 47 syl2anc ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) : ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –1-1-onto→ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
49 9 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( 𝐽 ↾t ℝ )
50 8 49 eqtri ⊢ 𝑇 = ( 𝐽 ↾t ℝ )
51 50 oveq1i ⊢ ( 𝑇 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( ( 𝐽 ↾t ℝ ) ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
52 9 cnfldtop ⊢ 𝐽 ∈ Top
53 7 40 sstrd ⊢ ( 𝜑 → ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ ℝ )
54 reex ⊢ ℝ ∈ V
55 54 a1i ⊢ ( 𝜑 → ℝ ∈ V )
56 restabs ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ ℝ ∧ ℝ ∈ V ) → ( ( 𝐽 ↾t ℝ ) ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝐽 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
57 52 53 55 56 mp3an2i ⊢ ( 𝜑 → ( ( 𝐽 ↾t ℝ ) ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝐽 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
58 51 57 eqtrid ⊢ ( 𝜑 → ( 𝑇 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝐽 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
59 40 5 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
60 6 rpred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
61 59 60 resubcld ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) ∈ ℝ )
62 59 60 readdcld ⊢ ( 𝜑 → ( 𝐶 + 𝑅 ) ∈ ℝ )
63 eqid ⊢ ( 𝑇 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑇 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
64 8 63 icccmp ⊢ ( ( ( 𝐶 − 𝑅 ) ∈ ℝ ∧ ( 𝐶 + 𝑅 ) ∈ ℝ ) → ( 𝑇 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ Comp )
65 61 62 64 syl2anc ⊢ ( 𝜑 → ( 𝑇 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ Comp )
66 58 65 eqeltrrd ⊢ ( 𝜑 → ( 𝐽 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ Comp )
67 f1of ⊢ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) : ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –1-1-onto→ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) → ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) : ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⟶ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
68 48 67 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) : ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⟶ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
69 19 41 sstrdi ⊢ ( 𝜑 → ran 𝐹 ⊆ ℂ )
70 21 69 sstrid ⊢ ( 𝜑 → ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ℂ )
71 rescncf ⊢ ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ 𝑋 → ( 𝐹 ∈ ( 𝑋 –cn→ ℝ ) → ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –cn→ ℝ ) ) )
72 7 1 71 sylc ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –cn→ ℝ ) )
73 cncfcdm ⊢ ( ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ℂ ∧ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –cn→ ℝ ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –cn→ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ↔ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) : ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⟶ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
74 70 72 73 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –cn→ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ↔ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) : ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⟶ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
75 68 74 mpbird ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –cn→ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
76 eqid ⊢ ( 𝐽 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝐽 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
77 9 76 cncfcnvcn ⊢ ( ( ( 𝐽 ↾t ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ Comp ∧ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –cn→ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) : ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –1-1-onto→ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ↔ ◡ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) –cn→ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
78 66 75 77 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) : ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –1-1-onto→ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ↔ ◡ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) –cn→ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
79 48 78 mpbid ⊢ ( 𝜑 → ◡ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) –cn→ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
80 44 79 sseldd ⊢ ( 𝜑 → ◡ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) –cn→ 𝑋 ) )
81 eqid ⊢ ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
82 9 81 10 cncfcn ⊢ ( ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ℂ ∧ 𝑋 ⊆ ℂ ) → ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) –cn→ 𝑋 ) = ( ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) Cn 𝑀 ) )
83 70 42 82 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) –cn→ 𝑋 ) = ( ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) Cn 𝑀 ) )
84 80 83 eleqtrd ⊢ ( 𝜑 → ◡ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) Cn 𝑀 ) )
85 59 6 ltsubrpd ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) < 𝐶 )
86 61 59 85 ltled ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) ≤ 𝐶 )
87 59 6 ltaddrpd ⊢ ( 𝜑 → 𝐶 < ( 𝐶 + 𝑅 ) )
88 59 62 87 ltled ⊢ ( 𝜑 → 𝐶 ≤ ( 𝐶 + 𝑅 ) )
89 elicc2 ⊢ ( ( ( 𝐶 − 𝑅 ) ∈ ℝ ∧ ( 𝐶 + 𝑅 ) ∈ ℝ ) → ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ↔ ( 𝐶 ∈ ℝ ∧ ( 𝐶 − 𝑅 ) ≤ 𝐶 ∧ 𝐶 ≤ ( 𝐶 + 𝑅 ) ) ) )
90 61 62 89 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ↔ ( 𝐶 ∈ ℝ ∧ ( 𝐶 − 𝑅 ) ≤ 𝐶 ∧ 𝐶 ≤ ( 𝐶 + 𝑅 ) ) ) )
91 59 86 88 90 mpbir3and ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
92 ffun ⊢ ( 𝐹 : 𝑋 ⟶ ℝ → Fun 𝐹 )
93 1 17 92 3syl ⊢ ( 𝜑 → Fun 𝐹 )
94 fdm ⊢ ( 𝐹 : 𝑋 ⟶ ℝ → dom 𝐹 = 𝑋 )
95 1 17 94 3syl ⊢ ( 𝜑 → dom 𝐹 = 𝑋 )
96 7 95 sseqtrrd ⊢ ( 𝜑 → ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ dom 𝐹 )
97 funfvima2 ⊢ ( ( Fun 𝐹 ∧ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ dom 𝐹 ) → ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
98 93 96 97 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
99 91 98 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
100 9 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
101 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ℂ ) → ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∈ ( TopOn ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
102 100 70 101 sylancr ⊢ ( 𝜑 → ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∈ ( TopOn ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
103 toponuni ⊢ ( ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∈ ( TopOn ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ∪ ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
104 102 103 syl ⊢ ( 𝜑 → ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ∪ ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
105 99 104 eleqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ∪ ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
106 eqid ⊢ ∪ ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ∪ ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
107 106 cncnpi ⊢ ( ( ◡ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) Cn 𝑀 ) ∧ ( 𝐹 ‘ 𝐶 ) ∈ ∪ ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ) → ◡ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) )
108 84 105 107 syl2anc ⊢ ( 𝜑 → ◡ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) )
109 38 108 eqeltrrd ⊢ ( 𝜑 → ( ◡ 𝐹 ↾ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∈ ( ( ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) )
110 11 oveq1i ⊢ ( 𝑁 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( ( 𝐽 ↾t 𝑌 ) ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
111 ssexg ⊢ ( ( 𝑌 ⊆ ℝ ∧ ℝ ∈ V ) → 𝑌 ∈ V )
112 20 54 111 sylancl ⊢ ( 𝜑 → 𝑌 ∈ V )
113 restabs ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ 𝑌 ∧ 𝑌 ∈ V ) → ( ( 𝐽 ↾t 𝑌 ) ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
114 52 22 112 113 mp3an2i ⊢ ( 𝜑 → ( ( 𝐽 ↾t 𝑌 ) ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
115 110 114 eqtrid ⊢ ( 𝜑 → ( 𝑁 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
116 115 oveq1d ⊢ ( 𝜑 → ( ( 𝑁 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) CnP 𝑀 ) = ( ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) CnP 𝑀 ) )
117 116 fveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) = ( ( ( 𝐽 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) )
118 109 117 eleqtrrd ⊢ ( 𝜑 → ( ◡ 𝐹 ↾ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∈ ( ( ( 𝑁 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) )
119 20 41 sstrdi ⊢ ( 𝜑 → 𝑌 ⊆ ℂ )
120 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑌 ⊆ ℂ ) → ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
121 100 119 120 sylancr ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
122 11 121 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ( TopOn ‘ 𝑌 ) )
123 topontop ⊢ ( 𝑁 ∈ ( TopOn ‘ 𝑌 ) → 𝑁 ∈ Top )
124 122 123 syl ⊢ ( 𝜑 → 𝑁 ∈ Top )
125 toponuni ⊢ ( 𝑁 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝑁 )
126 122 125 syl ⊢ ( 𝜑 → 𝑌 = ∪ 𝑁 )
127 22 126 sseqtrd ⊢ ( 𝜑 → ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ∪ 𝑁 )
128 22 20 sstrd ⊢ ( 𝜑 → ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ℝ )
129 difssd ⊢ ( 𝜑 → ( ℝ ∖ 𝑌 ) ⊆ ℝ )
130 128 129 unssd ⊢ ( 𝜑 → ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∪ ( ℝ ∖ 𝑌 ) ) ⊆ ℝ )
131 ssun1 ⊢ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∪ ( ℝ ∖ 𝑌 ) )
132 131 a1i ⊢ ( 𝜑 → ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∪ ( ℝ ∖ 𝑌 ) ) )
133 25 ntrss ⊢ ( ( 𝑇 ∈ Top ∧ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∪ ( ℝ ∖ 𝑌 ) ) ⊆ ℝ ∧ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∪ ( ℝ ∖ 𝑌 ) ) ) → ( ( int ‘ 𝑇 ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ⊆ ( ( int ‘ 𝑇 ) ‘ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∪ ( ℝ ∖ 𝑌 ) ) ) )
134 13 130 132 133 mp3an2i ⊢ ( 𝜑 → ( ( int ‘ 𝑇 ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ⊆ ( ( int ‘ 𝑇 ) ‘ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∪ ( ℝ ∖ 𝑌 ) ) ) )
135 134 31 sseldd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ 𝑇 ) ‘ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∪ ( ℝ ∖ 𝑌 ) ) ) )
136 f1of ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
137 4 136 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
138 137 5 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ 𝑌 )
139 135 138 elind ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( ( ( int ‘ 𝑇 ) ‘ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∪ ( ℝ ∖ 𝑌 ) ) ) ∩ 𝑌 ) )
140 eqid ⊢ ( 𝑇 ↾t 𝑌 ) = ( 𝑇 ↾t 𝑌 )
141 25 140 restntr ⊢ ( ( 𝑇 ∈ Top ∧ 𝑌 ⊆ ℝ ∧ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ 𝑌 ) → ( ( int ‘ ( 𝑇 ↾t 𝑌 ) ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( ( ( int ‘ 𝑇 ) ‘ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∪ ( ℝ ∖ 𝑌 ) ) ) ∩ 𝑌 ) )
142 13 20 22 141 mp3an2i ⊢ ( 𝜑 → ( ( int ‘ ( 𝑇 ↾t 𝑌 ) ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( ( ( int ‘ 𝑇 ) ‘ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∪ ( ℝ ∖ 𝑌 ) ) ) ∩ 𝑌 ) )
143 restabs ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ ℝ ∧ ℝ ∈ V ) → ( ( 𝐽 ↾t ℝ ) ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 ) )
144 52 20 55 143 mp3an2i ⊢ ( 𝜑 → ( ( 𝐽 ↾t ℝ ) ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 ) )
145 50 oveq1i ⊢ ( 𝑇 ↾t 𝑌 ) = ( ( 𝐽 ↾t ℝ ) ↾t 𝑌 )
146 144 145 11 3eqtr4g ⊢ ( 𝜑 → ( 𝑇 ↾t 𝑌 ) = 𝑁 )
147 146 fveq2d ⊢ ( 𝜑 → ( int ‘ ( 𝑇 ↾t 𝑌 ) ) = ( int ‘ 𝑁 ) )
148 147 fveq1d ⊢ ( 𝜑 → ( ( int ‘ ( 𝑇 ↾t 𝑌 ) ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( ( int ‘ 𝑁 ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
149 142 148 eqtr3d ⊢ ( 𝜑 → ( ( ( int ‘ 𝑇 ) ‘ ( ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∪ ( ℝ ∖ 𝑌 ) ) ) ∩ 𝑌 ) = ( ( int ‘ 𝑁 ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
150 139 149 eleqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ 𝑁 ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
151 126 feq2d ⊢ ( 𝜑 → ( ◡ 𝐹 : 𝑌 ⟶ 𝑋 ↔ ◡ 𝐹 : ∪ 𝑁 ⟶ 𝑋 ) )
152 35 151 mpbid ⊢ ( 𝜑 → ◡ 𝐹 : ∪ 𝑁 ⟶ 𝑋 )
153 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑋 ⊆ ℂ ) → ( 𝐽 ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
154 100 42 153 sylancr ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
155 10 154 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑋 ) )
156 toponuni ⊢ ( 𝑀 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝑀 )
157 feq3 ⊢ ( 𝑋 = ∪ 𝑀 → ( ◡ 𝐹 : ∪ 𝑁 ⟶ 𝑋 ↔ ◡ 𝐹 : ∪ 𝑁 ⟶ ∪ 𝑀 ) )
158 155 156 157 3syl ⊢ ( 𝜑 → ( ◡ 𝐹 : ∪ 𝑁 ⟶ 𝑋 ↔ ◡ 𝐹 : ∪ 𝑁 ⟶ ∪ 𝑀 ) )
159 152 158 mpbid ⊢ ( 𝜑 → ◡ 𝐹 : ∪ 𝑁 ⟶ ∪ 𝑀 )
160 eqid ⊢ ∪ 𝑁 = ∪ 𝑁
161 eqid ⊢ ∪ 𝑀 = ∪ 𝑀
162 160 161 cnprest ⊢ ( ( ( 𝑁 ∈ Top ∧ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ⊆ ∪ 𝑁 ) ∧ ( ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ 𝑁 ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∧ ◡ 𝐹 : ∪ 𝑁 ⟶ ∪ 𝑀 ) ) → ( ◡ 𝐹 ∈ ( ( 𝑁 CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) ↔ ( ◡ 𝐹 ↾ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∈ ( ( ( 𝑁 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) ) )
163 124 127 150 159 162 syl22anc ⊢ ( 𝜑 → ( ◡ 𝐹 ∈ ( ( 𝑁 CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) ↔ ( ◡ 𝐹 ↾ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∈ ( ( ( 𝑁 ↾t ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) ) )
164 118 163 mpbird ⊢ ( 𝜑 → ◡ 𝐹 ∈ ( ( 𝑁 CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) )
165 32 164 jca ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ 𝑇 ) ‘ 𝑌 ) ∧ ◡ 𝐹 ∈ ( ( 𝑁 CnP 𝑀 ) ‘ ( 𝐹 ‘ 𝐶 ) ) ) )