Metamath Proof Explorer

Theorem dvcnvrelem1

Description: Lemma for dvcnvre . (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→ 𝑌 )
dvcnvre.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
dvcnvre.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
dvcnvre.s ⊢ ( 𝜑 → ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ 𝑋 )
Assertion dvcnvrelem1 ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )

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 dvbsss ⊢ dom ( ℝ D 𝐹 ) ⊆ ℝ
9 2 8 eqsstrrdi ⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
10 9 5 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
11 6 rpred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
12 10 11 resubcld ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) ∈ ℝ )
13 10 11 readdcld ⊢ ( 𝜑 → ( 𝐶 + 𝑅 ) ∈ ℝ )
14 10 6 ltsubrpd ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) < 𝐶 )
15 10 6 ltaddrpd ⊢ ( 𝜑 → 𝐶 < ( 𝐶 + 𝑅 ) )
16 12 10 13 14 15 lttrd ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) < ( 𝐶 + 𝑅 ) )
17 12 13 16 ltled ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) ≤ ( 𝐶 + 𝑅 ) )
18 rescncf ⊢ ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ 𝑋 → ( 𝐹 ∈ ( 𝑋 –cn→ ℝ ) → ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –cn→ ℝ ) ) )
19 7 1 18 sylc ⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ∈ ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) –cn→ ℝ ) )
20 12 13 17 19 evthicc2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) )
21 cncff ⊢ ( 𝐹 ∈ ( 𝑋 –cn→ ℝ ) → 𝐹 : 𝑋 ⟶ ℝ )
22 1 21 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
23 22 5 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℝ )
24 23 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℝ )
25 12 rexrd ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) ∈ ℝ* )
26 13 rexrd ⊢ ( 𝜑 → ( 𝐶 + 𝑅 ) ∈ ℝ* )
27 lbicc2 ⊢ ( ( ( 𝐶 − 𝑅 ) ∈ ℝ* ∧ ( 𝐶 + 𝑅 ) ∈ ℝ* ∧ ( 𝐶 − 𝑅 ) ≤ ( 𝐶 + 𝑅 ) ) → ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
28 25 26 17 27 syl3anc ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
30 12 10 14 ltled ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) ≤ 𝐶 )
31 10 13 15 ltled ⊢ ( 𝜑 → 𝐶 ≤ ( 𝐶 + 𝑅 ) )
32 elicc2 ⊢ ( ( ( 𝐶 − 𝑅 ) ∈ ℝ ∧ ( 𝐶 + 𝑅 ) ∈ ℝ ) → ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ↔ ( 𝐶 ∈ ℝ ∧ ( 𝐶 − 𝑅 ) ≤ 𝐶 ∧ 𝐶 ≤ ( 𝐶 + 𝑅 ) ) ) )
33 12 13 32 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ↔ ( 𝐶 ∈ ℝ ∧ ( 𝐶 − 𝑅 ) ≤ 𝐶 ∧ 𝐶 ≤ ( 𝐶 + 𝑅 ) ) ) )
34 10 30 31 33 mpbir3and ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
36 14 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐶 − 𝑅 ) < 𝐶 )
37 isorel ⊢ ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∧ ( ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ∧ 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐶 − 𝑅 ) < 𝐶 ↔ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ) )
38 37 biimpd ⊢ ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∧ ( ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ∧ 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐶 − 𝑅 ) < 𝐶 → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ) )
39 38 exp32 ⊢ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( ( 𝐶 − 𝑅 ) < 𝐶 → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ) ) ) )
40 39 com4l ⊢ ( ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( ( 𝐶 − 𝑅 ) < 𝐶 → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ) ) ) )
41 29 35 36 40 syl3c ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ) )
42 29 fvresd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) = ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) )
43 35 fvresd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) = ( 𝐹 ‘ 𝐶 ) )
44 42 43 breq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ↔ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) < ( 𝐹 ‘ 𝐶 ) ) )
45 41 44 sylibd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) < ( 𝐹 ‘ 𝐶 ) ) )
46 22 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → 𝐹 : 𝑋 ⟶ ℝ )
47 46 ffund ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → Fun 𝐹 )
48 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ 𝑋 )
49 46 fdmd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → dom 𝐹 = 𝑋 )
50 48 49 sseqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ dom 𝐹 )
51 funfvima2 ⊢ ( ( Fun 𝐹 ∧ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ dom 𝐹 ) → ( ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
52 47 50 51 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
53 29 52 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
54 df-ima ⊢ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
55 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) )
56 54 55 eqtrid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) )
57 53 56 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ( 𝑥 [,] 𝑦 ) )
58 elicc2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ( 𝑥 [,] 𝑦 ) ↔ ( ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ℝ ∧ 𝑥 ≤ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ≤ 𝑦 ) ) )
59 58 ad2antrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ( 𝑥 [,] 𝑦 ) ↔ ( ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ℝ ∧ 𝑥 ≤ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ≤ 𝑦 ) ) )
60 57 59 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ℝ ∧ 𝑥 ≤ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ≤ 𝑦 ) )
61 60 simp2d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → 𝑥 ≤ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) )
62 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → 𝑥 ∈ ℝ )
63 7 28 sseldd ⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) ∈ 𝑋 )
64 22 63 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ℝ )
65 64 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ℝ )
66 lelttr ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐶 ) ∈ ℝ ) → ( ( 𝑥 ≤ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) < ( 𝐹 ‘ 𝐶 ) ) → 𝑥 < ( 𝐹 ‘ 𝐶 ) ) )
67 62 65 24 66 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝑥 ≤ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) < ( 𝐹 ‘ 𝐶 ) ) → 𝑥 < ( 𝐹 ‘ 𝐶 ) ) )
68 61 67 mpand ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) < ( 𝐹 ‘ 𝐶 ) → 𝑥 < ( 𝐹 ‘ 𝐶 ) ) )
69 45 68 syld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → 𝑥 < ( 𝐹 ‘ 𝐶 ) ) )
70 ubicc2 ⊢ ( ( ( 𝐶 − 𝑅 ) ∈ ℝ* ∧ ( 𝐶 + 𝑅 ) ∈ ℝ* ∧ ( 𝐶 − 𝑅 ) ≤ ( 𝐶 + 𝑅 ) ) → ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
71 25 26 17 70 syl3anc ⊢ ( 𝜑 → ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) )
73 15 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → 𝐶 < ( 𝐶 + 𝑅 ) )
74 isorel ⊢ ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∧ ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ∧ ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐶 < ( 𝐶 + 𝑅 ) ↔ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ) )
75 74 biimpd ⊢ ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∧ ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ∧ ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐶 < ( 𝐶 + 𝑅 ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ) )
76 75 exp32 ⊢ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐶 < ( 𝐶 + 𝑅 ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ) ) ) )
77 76 com4l ⊢ ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐶 < ( 𝐶 + 𝑅 ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ) ) ) )
78 35 72 73 77 syl3c ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ) )
79 fvex ⊢ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ∈ V
80 fvex ⊢ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ∈ V
81 79 80 brcnv ⊢ ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ↔ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) )
82 72 fvresd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) = ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) )
83 82 43 breq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ↔ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) < ( 𝐹 ‘ 𝐶 ) ) )
84 81 83 syl5bb ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ↔ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) < ( 𝐹 ‘ 𝐶 ) ) )
85 78 84 sylibd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) < ( 𝐹 ‘ 𝐶 ) ) )
86 funfvima2 ⊢ ( ( Fun 𝐹 ∧ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ dom 𝐹 ) → ( ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
87 47 50 86 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
88 72 87 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) )
89 88 56 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ( 𝑥 [,] 𝑦 ) )
90 elicc2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ( 𝑥 [,] 𝑦 ) ↔ ( ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ℝ ∧ 𝑥 ≤ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ≤ 𝑦 ) ) )
91 90 ad2antrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ( 𝑥 [,] 𝑦 ) ↔ ( ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ℝ ∧ 𝑥 ≤ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ≤ 𝑦 ) ) )
92 89 91 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ℝ ∧ 𝑥 ≤ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ≤ 𝑦 ) )
93 92 simp2d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → 𝑥 ≤ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) )
94 7 71 sseldd ⊢ ( 𝜑 → ( 𝐶 + 𝑅 ) ∈ 𝑋 )
95 22 94 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ℝ )
96 95 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ℝ )
97 lelttr ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐶 ) ∈ ℝ ) → ( ( 𝑥 ≤ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) < ( 𝐹 ‘ 𝐶 ) ) → 𝑥 < ( 𝐹 ‘ 𝐶 ) ) )
98 62 96 24 97 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝑥 ≤ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) < ( 𝐹 ‘ 𝐶 ) ) → 𝑥 < ( 𝐹 ‘ 𝐶 ) ) )
99 93 98 mpand ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) < ( 𝐹 ‘ 𝐶 ) → 𝑥 < ( 𝐹 ‘ 𝐶 ) ) )
100 85 99 syld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → 𝑥 < ( 𝐹 ‘ 𝐶 ) ) )
101 ax-resscn ⊢ ℝ ⊆ ℂ
102 101 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
103 fss ⊢ ( ( 𝐹 : 𝑋 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : 𝑋 ⟶ ℂ )
104 22 101 103 sylancl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
105 7 9 sstrd ⊢ ( 𝜑 → ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ ℝ )
106 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
107 106 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
108 106 107 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : 𝑋 ⟶ ℂ ) ∧ ( 𝑋 ⊆ ℝ ∧ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
109 102 104 9 105 108 syl22anc ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
110 iccntr ⊢ ( ( ( 𝐶 − 𝑅 ) ∈ ℝ ∧ ( 𝐶 + 𝑅 ) ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) )
111 12 13 110 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) )
112 111 reseq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ) )
113 109 112 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ) )
114 113 dmeqd ⊢ ( 𝜑 → dom ( ℝ D ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ) )
115 dmres ⊢ dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ) = ( ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ∩ dom ( ℝ D 𝐹 ) )
116 ioossicc ⊢ ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ⊆ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) )
117 116 7 sstrid ⊢ ( 𝜑 → ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ⊆ 𝑋 )
118 117 2 sseqtrrd ⊢ ( 𝜑 → ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ⊆ dom ( ℝ D 𝐹 ) )
119 df-ss ⊢ ( ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ⊆ dom ( ℝ D 𝐹 ) ↔ ( ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ∩ dom ( ℝ D 𝐹 ) ) = ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) )
120 118 119 sylib ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ∩ dom ( ℝ D 𝐹 ) ) = ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) )
121 115 120 eqtrid ⊢ ( 𝜑 → dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ) = ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) )
122 114 121 eqtrd ⊢ ( 𝜑 → dom ( ℝ D ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) )
123 resss ⊢ ( ( ℝ D 𝐹 ) ↾ ( ( 𝐶 − 𝑅 ) (,) ( 𝐶 + 𝑅 ) ) ) ⊆ ( ℝ D 𝐹 )
124 113 123 eqsstrdi ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ⊆ ( ℝ D 𝐹 ) )
125 rnss ⊢ ( ( ℝ D ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ⊆ ( ℝ D 𝐹 ) → ran ( ℝ D ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ⊆ ran ( ℝ D 𝐹 ) )
126 124 125 syl ⊢ ( 𝜑 → ran ( ℝ D ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ⊆ ran ( ℝ D 𝐹 ) )
127 126 3 ssneldd ⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
128 12 13 19 122 127 dvne0 ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∨ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ) )
129 128 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∨ ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ) )
130 69 100 129 mpjaod ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → 𝑥 < ( 𝐹 ‘ 𝐶 ) )
131 isorel ⊢ ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∧ ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ∧ ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐶 < ( 𝐶 + 𝑅 ) ↔ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ) )
132 131 biimpd ⊢ ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∧ ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ∧ ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐶 < ( 𝐶 + 𝑅 ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ) )
133 132 exp32 ⊢ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐶 < ( 𝐶 + 𝑅 ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ) ) ) )
134 133 com4l ⊢ ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( ( 𝐶 + 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐶 < ( 𝐶 + 𝑅 ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ) ) ) )
135 35 72 73 134 syl3c ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ) )
136 43 82 breq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 + 𝑅 ) ) ↔ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ) )
137 135 136 sylibd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ) )
138 92 simp3d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ≤ 𝑦 )
139 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → 𝑦 ∈ ℝ )
140 ltletr ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ∈ ℝ ∧ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ≤ 𝑦 ) → ( 𝐹 ‘ 𝐶 ) < 𝑦 ) )
141 24 96 139 140 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) ≤ 𝑦 ) → ( 𝐹 ‘ 𝐶 ) < 𝑦 ) )
142 138 141 mpan2d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ ( 𝐶 + 𝑅 ) ) → ( 𝐹 ‘ 𝐶 ) < 𝑦 ) )
143 137 142 syld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐹 ‘ 𝐶 ) < 𝑦 ) )
144 isorel ⊢ ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∧ ( ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ∧ 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐶 − 𝑅 ) < 𝐶 ↔ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ) )
145 144 biimpd ⊢ ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ∧ ( ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ∧ 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐶 − 𝑅 ) < 𝐶 → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ) )
146 145 exp32 ⊢ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( ( 𝐶 − 𝑅 ) < 𝐶 → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ) ) ) )
147 146 com4l ⊢ ( ( 𝐶 − 𝑅 ) ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( 𝐶 ∈ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) → ( ( 𝐶 − 𝑅 ) < 𝐶 → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ) ) ) )
148 29 35 36 147 syl3c ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ) )
149 fvex ⊢ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) ∈ V
150 149 79 brcnv ⊢ ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ↔ ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) )
151 43 42 breq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) ↔ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ) )
152 150 151 syl5bb ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ ( 𝐶 − 𝑅 ) ) ◡ < ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ‘ 𝐶 ) ↔ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ) )
153 148 152 sylibd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ) )
154 60 simp3d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ≤ 𝑦 )
155 ltletr ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ∈ ℝ ∧ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ≤ 𝑦 ) → ( 𝐹 ‘ 𝐶 ) < 𝑦 ) )
156 24 65 139 155 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ∧ ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) ≤ 𝑦 ) → ( 𝐹 ‘ 𝐶 ) < 𝑦 ) )
157 154 156 mpan2d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ ( 𝐶 − 𝑅 ) ) → ( 𝐹 ‘ 𝐶 ) < 𝑦 ) )
158 153 157 syld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) Isom < , ◡ < ( ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) , ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) → ( 𝐹 ‘ 𝐶 ) < 𝑦 ) )
159 143 158 129 mpjaod ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 ‘ 𝐶 ) < 𝑦 )
160 62 rexrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → 𝑥 ∈ ℝ* )
161 139 rexrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → 𝑦 ∈ ℝ* )
162 elioo2 ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝐹 ‘ 𝐶 ) ∈ ( 𝑥 (,) 𝑦 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ∈ ℝ ∧ 𝑥 < ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐶 ) < 𝑦 ) ) )
163 160 161 162 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ∈ ( 𝑥 (,) 𝑦 ) ↔ ( ( 𝐹 ‘ 𝐶 ) ∈ ℝ ∧ 𝑥 < ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐶 ) < 𝑦 ) ) )
164 24 130 159 163 mpbir3and ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ( 𝑥 (,) 𝑦 ) )
165 56 fveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑥 [,] 𝑦 ) ) )
166 iccntr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑥 [,] 𝑦 ) ) = ( 𝑥 (,) 𝑦 ) )
167 166 ad2antrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑥 [,] 𝑦 ) ) = ( 𝑥 (,) 𝑦 ) )
168 165 167 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) = ( 𝑥 (,) 𝑦 ) )
169 164 168 eleqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )
170 169 expr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) → ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ) )
171 170 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ran ( 𝐹 ↾ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) = ( 𝑥 [,] 𝑦 ) → ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) ) )
172 20 171 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐹 “ ( ( 𝐶 − 𝑅 ) [,] ( 𝐶 + 𝑅 ) ) ) ) )