This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnheiborlem

Description: Lemma for cnheibor . (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses cnheibor.2 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
cnheibor.3 ⊢ 𝑇 = ( 𝐽 ↾t 𝑋 )
cnheibor.4 ⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
cnheibor.5 ⊢ 𝑌 = ( 𝐹 “ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) )
Assertion cnheiborlem ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → 𝑇 ∈ Comp )

Proof

Step Hyp Ref Expression
1 cnheibor.2 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 cnheibor.3 ⊢ 𝑇 = ( 𝐽 ↾t 𝑋 )
3 cnheibor.4 ⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
4 cnheibor.5 ⊢ 𝑌 = ( 𝐹 “ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) )
5 1 cnfldtop ⊢ 𝐽 ∈ Top
6 3 cnref1o ⊢ 𝐹 : ( ℝ × ℝ ) –1-1-onto→ ℂ
7 f1ofn ⊢ ( 𝐹 : ( ℝ × ℝ ) –1-1-onto→ ℂ → 𝐹 Fn ( ℝ × ℝ ) )
8 elpreima ⊢ ( 𝐹 Fn ( ℝ × ℝ ) → ( 𝑢 ∈ ( ◡ 𝐹 “ 𝑋 ) ↔ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) )
9 6 7 8 mp2b ⊢ ( 𝑢 ∈ ( ◡ 𝐹 “ 𝑋 ) ↔ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) )
10 1st2nd2 ⊢ ( 𝑢 ∈ ( ℝ × ℝ ) → 𝑢 = ⟨ ( 1st ‘ 𝑢 ) , ( 2nd ‘ 𝑢 ) ⟩ )
11 10 ad2antrl ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → 𝑢 = ⟨ ( 1st ‘ 𝑢 ) , ( 2nd ‘ 𝑢 ) ⟩ )
12 xp1st ⊢ ( 𝑢 ∈ ( ℝ × ℝ ) → ( 1st ‘ 𝑢 ) ∈ ℝ )
13 12 ad2antrl ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 1st ‘ 𝑢 ) ∈ ℝ )
14 13 recnd ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 1st ‘ 𝑢 ) ∈ ℂ )
15 14 abscld ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( abs ‘ ( 1st ‘ 𝑢 ) ) ∈ ℝ )
16 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
17 16 toponunii ⊢ ℂ = ∪ 𝐽
18 17 cldss ⊢ ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) → 𝑋 ⊆ ℂ )
19 18 adantr ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → 𝑋 ⊆ ℂ )
20 19 adantr ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → 𝑋 ⊆ ℂ )
21 simprr ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 )
22 20 21 sseldd ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑢 ) ∈ ℂ )
23 22 abscld ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) ∈ ℝ )
24 simplrl ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → 𝑅 ∈ ℝ )
25 simprl ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → 𝑢 ∈ ( ℝ × ℝ ) )
26 f1ocnvfv1 ⊢ ( ( 𝐹 : ( ℝ × ℝ ) –1-1-onto→ ℂ ∧ 𝑢 ∈ ( ℝ × ℝ ) ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) = 𝑢 )
27 6 25 26 sylancr ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) = 𝑢 )
28 fveq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑢 ) → ( ℜ ‘ 𝑧 ) = ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) )
29 fveq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑢 ) → ( ℑ ‘ 𝑧 ) = ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) )
30 28 29 opeq12d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑢 ) → ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ = ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ⟩ )
31 3 cnrecnv ⊢ ◡ 𝐹 = ( 𝑧 ∈ ℂ ↦ ⟨ ( ℜ ‘ 𝑧 ) , ( ℑ ‘ 𝑧 ) ⟩ )
32 opex ⊢ ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ⟩ ∈ V
33 30 31 32 fvmpt ⊢ ( ( 𝐹 ‘ 𝑢 ) ∈ ℂ → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) = ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ⟩ )
34 22 33 syl ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) = ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ⟩ )
35 27 34 eqtr3d ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → 𝑢 = ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ⟩ )
36 35 fveq2d ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 1st ‘ 𝑢 ) = ( 1st ‘ ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ⟩ ) )
37 fvex ⊢ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) ∈ V
38 fvex ⊢ ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ∈ V
39 37 38 op1st ⊢ ( 1st ‘ ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ⟩ ) = ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) )
40 36 39 eqtrdi ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 1st ‘ 𝑢 ) = ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) )
41 40 fveq2d ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( abs ‘ ( 1st ‘ 𝑢 ) ) = ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) ) )
42 absrele ⊢ ( ( 𝐹 ‘ 𝑢 ) ∈ ℂ → ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) )
43 22 42 syl ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) )
44 41 43 eqbrtrd ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( abs ‘ ( 1st ‘ 𝑢 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) )
45 fveq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑢 ) → ( abs ‘ 𝑧 ) = ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) )
46 45 breq1d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑢 ) → ( ( abs ‘ 𝑧 ) ≤ 𝑅 ↔ ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) ≤ 𝑅 ) )
47 simplrr ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 )
48 46 47 21 rspcdva ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) ≤ 𝑅 )
49 15 23 24 44 48 letrd ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( abs ‘ ( 1st ‘ 𝑢 ) ) ≤ 𝑅 )
50 13 24 absled ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( ( abs ‘ ( 1st ‘ 𝑢 ) ) ≤ 𝑅 ↔ ( - 𝑅 ≤ ( 1st ‘ 𝑢 ) ∧ ( 1st ‘ 𝑢 ) ≤ 𝑅 ) ) )
51 49 50 mpbid ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( - 𝑅 ≤ ( 1st ‘ 𝑢 ) ∧ ( 1st ‘ 𝑢 ) ≤ 𝑅 ) )
52 51 simpld ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → - 𝑅 ≤ ( 1st ‘ 𝑢 ) )
53 51 simprd ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 1st ‘ 𝑢 ) ≤ 𝑅 )
54 renegcl ⊢ ( 𝑅 ∈ ℝ → - 𝑅 ∈ ℝ )
55 24 54 syl ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → - 𝑅 ∈ ℝ )
56 elicc2 ⊢ ( ( - 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( 1st ‘ 𝑢 ) ∈ ( - 𝑅 [,] 𝑅 ) ↔ ( ( 1st ‘ 𝑢 ) ∈ ℝ ∧ - 𝑅 ≤ ( 1st ‘ 𝑢 ) ∧ ( 1st ‘ 𝑢 ) ≤ 𝑅 ) ) )
57 55 24 56 syl2anc ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( ( 1st ‘ 𝑢 ) ∈ ( - 𝑅 [,] 𝑅 ) ↔ ( ( 1st ‘ 𝑢 ) ∈ ℝ ∧ - 𝑅 ≤ ( 1st ‘ 𝑢 ) ∧ ( 1st ‘ 𝑢 ) ≤ 𝑅 ) ) )
58 13 52 53 57 mpbir3and ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 1st ‘ 𝑢 ) ∈ ( - 𝑅 [,] 𝑅 ) )
59 xp2nd ⊢ ( 𝑢 ∈ ( ℝ × ℝ ) → ( 2nd ‘ 𝑢 ) ∈ ℝ )
60 59 ad2antrl ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 2nd ‘ 𝑢 ) ∈ ℝ )
61 60 recnd ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 2nd ‘ 𝑢 ) ∈ ℂ )
62 61 abscld ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( abs ‘ ( 2nd ‘ 𝑢 ) ) ∈ ℝ )
63 35 fveq2d ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 2nd ‘ 𝑢 ) = ( 2nd ‘ ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ⟩ ) )
64 37 38 op2nd ⊢ ( 2nd ‘ ⟨ ( ℜ ‘ ( 𝐹 ‘ 𝑢 ) ) , ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ⟩ ) = ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) )
65 63 64 eqtrdi ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 2nd ‘ 𝑢 ) = ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) )
66 65 fveq2d ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( abs ‘ ( 2nd ‘ 𝑢 ) ) = ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ) )
67 absimle ⊢ ( ( 𝐹 ‘ 𝑢 ) ∈ ℂ → ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) )
68 22 67 syl ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑢 ) ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) )
69 66 68 eqbrtrd ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( abs ‘ ( 2nd ‘ 𝑢 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) )
70 62 23 24 69 48 letrd ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( abs ‘ ( 2nd ‘ 𝑢 ) ) ≤ 𝑅 )
71 60 24 absled ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( ( abs ‘ ( 2nd ‘ 𝑢 ) ) ≤ 𝑅 ↔ ( - 𝑅 ≤ ( 2nd ‘ 𝑢 ) ∧ ( 2nd ‘ 𝑢 ) ≤ 𝑅 ) ) )
72 70 71 mpbid ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( - 𝑅 ≤ ( 2nd ‘ 𝑢 ) ∧ ( 2nd ‘ 𝑢 ) ≤ 𝑅 ) )
73 72 simpld ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → - 𝑅 ≤ ( 2nd ‘ 𝑢 ) )
74 72 simprd ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 2nd ‘ 𝑢 ) ≤ 𝑅 )
75 elicc2 ⊢ ( ( - 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( 2nd ‘ 𝑢 ) ∈ ( - 𝑅 [,] 𝑅 ) ↔ ( ( 2nd ‘ 𝑢 ) ∈ ℝ ∧ - 𝑅 ≤ ( 2nd ‘ 𝑢 ) ∧ ( 2nd ‘ 𝑢 ) ≤ 𝑅 ) ) )
76 55 24 75 syl2anc ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( ( 2nd ‘ 𝑢 ) ∈ ( - 𝑅 [,] 𝑅 ) ↔ ( ( 2nd ‘ 𝑢 ) ∈ ℝ ∧ - 𝑅 ≤ ( 2nd ‘ 𝑢 ) ∧ ( 2nd ‘ 𝑢 ) ≤ 𝑅 ) ) )
77 60 73 74 76 mpbir3and ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ( 2nd ‘ 𝑢 ) ∈ ( - 𝑅 [,] 𝑅 ) )
78 58 77 opelxpd ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → ⟨ ( 1st ‘ 𝑢 ) , ( 2nd ‘ 𝑢 ) ⟩ ∈ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) )
79 11 78 eqeltrd ⊢ ( ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) ∧ ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) ) → 𝑢 ∈ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) )
80 79 ex ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → ( ( 𝑢 ∈ ( ℝ × ℝ ) ∧ ( 𝐹 ‘ 𝑢 ) ∈ 𝑋 ) → 𝑢 ∈ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) )
81 9 80 biimtrid ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → ( 𝑢 ∈ ( ◡ 𝐹 “ 𝑋 ) → 𝑢 ∈ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) )
82 81 ssrdv ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → ( ◡ 𝐹 “ 𝑋 ) ⊆ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) )
83 f1ofun ⊢ ( 𝐹 : ( ℝ × ℝ ) –1-1-onto→ ℂ → Fun 𝐹 )
84 6 83 ax-mp ⊢ Fun 𝐹
85 f1ofo ⊢ ( 𝐹 : ( ℝ × ℝ ) –1-1-onto→ ℂ → 𝐹 : ( ℝ × ℝ ) –onto→ ℂ )
86 forn ⊢ ( 𝐹 : ( ℝ × ℝ ) –onto→ ℂ → ran 𝐹 = ℂ )
87 6 85 86 mp2b ⊢ ran 𝐹 = ℂ
88 19 87 sseqtrrdi ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → 𝑋 ⊆ ran 𝐹 )
89 funimass1 ⊢ ( ( Fun 𝐹 ∧ 𝑋 ⊆ ran 𝐹 ) → ( ( ◡ 𝐹 “ 𝑋 ) ⊆ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) → 𝑋 ⊆ ( 𝐹 “ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) ) )
90 84 88 89 sylancr ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → ( ( ◡ 𝐹 “ 𝑋 ) ⊆ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) → 𝑋 ⊆ ( 𝐹 “ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) ) )
91 82 90 mpd ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → 𝑋 ⊆ ( 𝐹 “ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) )
92 91 4 sseqtrrdi ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → 𝑋 ⊆ 𝑌 )
93 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
94 3 93 1 cnrehmeo ⊢ 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Homeo 𝐽 )
95 imaexg ⊢ ( 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Homeo 𝐽 ) → ( 𝐹 “ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) ∈ V )
96 94 95 ax-mp ⊢ ( 𝐹 “ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) ∈ V
97 4 96 eqeltri ⊢ 𝑌 ∈ V
98 97 a1i ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → 𝑌 ∈ V )
99 restabs ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ V ) → ( ( 𝐽 ↾t 𝑌 ) ↾t 𝑋 ) = ( 𝐽 ↾t 𝑋 ) )
100 5 92 98 99 mp3an2i ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → ( ( 𝐽 ↾t 𝑌 ) ↾t 𝑋 ) = ( 𝐽 ↾t 𝑋 ) )
101 100 2 eqtr4di ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → ( ( 𝐽 ↾t 𝑌 ) ↾t 𝑋 ) = 𝑇 )
102 4 oveq2i ⊢ ( 𝐽 ↾t 𝑌 ) = ( 𝐽 ↾t ( 𝐹 “ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) )
103 ishmeo ⊢ ( 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Homeo 𝐽 ) ↔ ( 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Cn 𝐽 ) ∧ ◡ 𝐹 ∈ ( 𝐽 Cn ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) ) ) )
104 94 103 mpbi ⊢ ( 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Cn 𝐽 ) ∧ ◡ 𝐹 ∈ ( 𝐽 Cn ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) ) )
105 104 simpli ⊢ 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Cn 𝐽 )
106 iccssre ⊢ ( ( - 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( - 𝑅 [,] 𝑅 ) ⊆ ℝ )
107 54 106 mpancom ⊢ ( 𝑅 ∈ ℝ → ( - 𝑅 [,] 𝑅 ) ⊆ ℝ )
108 1 93 rerest ⊢ ( ( - 𝑅 [,] 𝑅 ) ⊆ ℝ → ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( - 𝑅 [,] 𝑅 ) ) )
109 107 108 syl ⊢ ( 𝑅 ∈ ℝ → ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( - 𝑅 [,] 𝑅 ) ) )
110 109 109 oveq12d ⊢ ( 𝑅 ∈ ℝ → ( ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) ×t ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) ) = ( ( ( topGen ‘ ran (,) ) ↾t ( - 𝑅 [,] 𝑅 ) ) ×t ( ( topGen ‘ ran (,) ) ↾t ( - 𝑅 [,] 𝑅 ) ) ) )
111 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
112 ovex ⊢ ( - 𝑅 [,] 𝑅 ) ∈ V
113 txrest ⊢ ( ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( topGen ‘ ran (,) ) ∈ Top ) ∧ ( ( - 𝑅 [,] 𝑅 ) ∈ V ∧ ( - 𝑅 [,] 𝑅 ) ∈ V ) ) → ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) ↾t ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) = ( ( ( topGen ‘ ran (,) ) ↾t ( - 𝑅 [,] 𝑅 ) ) ×t ( ( topGen ‘ ran (,) ) ↾t ( - 𝑅 [,] 𝑅 ) ) ) )
114 111 111 112 112 113 mp4an ⊢ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) ↾t ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) = ( ( ( topGen ‘ ran (,) ) ↾t ( - 𝑅 [,] 𝑅 ) ) ×t ( ( topGen ‘ ran (,) ) ↾t ( - 𝑅 [,] 𝑅 ) ) )
115 110 114 eqtr4di ⊢ ( 𝑅 ∈ ℝ → ( ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) ×t ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) ) = ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) ↾t ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) )
116 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( - 𝑅 [,] 𝑅 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( - 𝑅 [,] 𝑅 ) )
117 93 116 icccmp ⊢ ( ( - 𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾t ( - 𝑅 [,] 𝑅 ) ) ∈ Comp )
118 54 117 mpancom ⊢ ( 𝑅 ∈ ℝ → ( ( topGen ‘ ran (,) ) ↾t ( - 𝑅 [,] 𝑅 ) ) ∈ Comp )
119 109 118 eqeltrd ⊢ ( 𝑅 ∈ ℝ → ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) ∈ Comp )
120 txcmp ⊢ ( ( ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) ∈ Comp ∧ ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) ∈ Comp ) → ( ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) ×t ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) ) ∈ Comp )
121 119 119 120 syl2anc ⊢ ( 𝑅 ∈ ℝ → ( ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) ×t ( 𝐽 ↾t ( - 𝑅 [,] 𝑅 ) ) ) ∈ Comp )
122 115 121 eqeltrrd ⊢ ( 𝑅 ∈ ℝ → ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) ↾t ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) ∈ Comp )
123 imacmp ⊢ ( ( 𝐹 ∈ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) Cn 𝐽 ) ∧ ( ( ( topGen ‘ ran (,) ) ×t ( topGen ‘ ran (,) ) ) ↾t ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) ∈ Comp ) → ( 𝐽 ↾t ( 𝐹 “ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) ) ∈ Comp )
124 105 122 123 sylancr ⊢ ( 𝑅 ∈ ℝ → ( 𝐽 ↾t ( 𝐹 “ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) ) ∈ Comp )
125 102 124 eqeltrid ⊢ ( 𝑅 ∈ ℝ → ( 𝐽 ↾t 𝑌 ) ∈ Comp )
126 125 ad2antrl ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → ( 𝐽 ↾t 𝑌 ) ∈ Comp )
127 imassrn ⊢ ( 𝐹 “ ( ( - 𝑅 [,] 𝑅 ) × ( - 𝑅 [,] 𝑅 ) ) ) ⊆ ran 𝐹
128 4 127 eqsstri ⊢ 𝑌 ⊆ ran 𝐹
129 f1of ⊢ ( 𝐹 : ( ℝ × ℝ ) –1-1-onto→ ℂ → 𝐹 : ( ℝ × ℝ ) ⟶ ℂ )
130 frn ⊢ ( 𝐹 : ( ℝ × ℝ ) ⟶ ℂ → ran 𝐹 ⊆ ℂ )
131 6 129 130 mp2b ⊢ ran 𝐹 ⊆ ℂ
132 128 131 sstri ⊢ 𝑌 ⊆ ℂ
133 simpl ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
134 17 restcldi ⊢ ( ( 𝑌 ⊆ ℂ ∧ 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑋 ⊆ 𝑌 ) → 𝑋 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑌 ) ) )
135 132 133 92 134 mp3an2i ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → 𝑋 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑌 ) ) )
136 cmpcld ⊢ ( ( ( 𝐽 ↾t 𝑌 ) ∈ Comp ∧ 𝑋 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑌 ) ) ) → ( ( 𝐽 ↾t 𝑌 ) ↾t 𝑋 ) ∈ Comp )
137 126 135 136 syl2anc ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → ( ( 𝐽 ↾t 𝑌 ) ↾t 𝑋 ) ∈ Comp )
138 101 137 eqeltrrd ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑅 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑋 ( abs ‘ 𝑧 ) ≤ 𝑅 ) ) → 𝑇 ∈ Comp )