Metamath Proof Explorer

Theorem rlimresb

Description: The restriction of a function to an unbounded-above interval converges iff the original converges. (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Hypotheses rlimresb.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
rlimresb.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
rlimresb.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion rlimresb ( 𝜑 → ( 𝐹 ⇝𝑟 𝐶 ↔ ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ⇝𝑟 𝐶 ) )

Proof

Step Hyp Ref Expression
1 rlimresb.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 rlimresb.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 rlimresb.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 rlimcl ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ )
5 4 a1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ ) )
6 rlimcl ⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ )
7 6 a1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ ) )
8 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥 ) ) ) → 𝐴 ⊆ ℝ )
9 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥 ) ) ) → 𝑥 ∈ 𝐴 )
10 8 9 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
11 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥 ) ) ) → 𝐵 ∈ ℝ )
12 elicopnf ⊢ ( 𝐵 ∈ ℝ → ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ↔ ( 𝑧 ∈ ℝ ∧ 𝐵 ≤ 𝑧 ) ) )
13 3 12 syl ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ↔ ( 𝑧 ∈ ℝ ∧ 𝐵 ≤ 𝑧 ) ) )
14 13 biimpa ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 [,) +∞ ) ) → ( 𝑧 ∈ ℝ ∧ 𝐵 ≤ 𝑧 ) )
15 14 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥 ) ) ) → ( 𝑧 ∈ ℝ ∧ 𝐵 ≤ 𝑧 ) )
16 15 simpld ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥 ) ) ) → 𝑧 ∈ ℝ )
17 15 simprd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥 ) ) ) → 𝐵 ≤ 𝑧 )
18 simprrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥 ) ) ) → 𝑧 ≤ 𝑥 )
19 11 16 10 17 18 letrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥 ) ) ) → 𝐵 ≤ 𝑥 )
20 elicopnf ⊢ ( 𝐵 ∈ ℝ → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐵 ≤ 𝑥 ) ) )
21 11 20 syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥 ) ) ) → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐵 ≤ 𝑥 ) ) )
22 10 19 21 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝐵 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥 ) ) ) → 𝑥 ∈ ( 𝐵 [,) +∞ ) )
23 22 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥 ) ) → 𝑥 ∈ ( 𝐵 [,) +∞ ) )
24 23 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ≤ 𝑥 ) → 𝑥 ∈ ( 𝐵 [,) +∞ ) )
25 biimt ⊢ ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ↔ ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) )
26 24 25 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ≤ 𝑥 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ↔ ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) )
27 26 pm5.74da ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ↔ ( 𝑧 ≤ 𝑥 → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) ) )
28 bi2.04 ⊢ ( ( 𝑧 ≤ 𝑥 → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) ↔ ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) )
29 27 28 bitrdi ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ↔ ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) ) )
30 29 pm5.74da ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 [,) +∞ ) ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) ) ) )
31 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 [,) +∞ ) ) )
32 31 imbi1i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 [,) +∞ ) ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) )
33 impexp ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 [,) +∞ ) ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) ) )
34 32 33 bitri ⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) ) )
35 30 34 bitr4di ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 [,) +∞ ) ) → ( ( 𝑥 ∈ 𝐴 → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) ) )
36 35 ralbidv2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐵 [,) +∞ ) ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) )
37 36 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) )
38 37 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) )
40 1 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
41 40 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
43 2 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → 𝐴 ⊆ ℝ )
44 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
45 3 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℝ )
46 42 43 44 45 rlim3 ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) )
47 elinel1 ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) → 𝑥 ∈ 𝐴 )
48 47 40 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
49 48 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
51 inss1 ⊢ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ⊆ 𝐴
52 51 2 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ⊆ ℝ )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ⊆ ℝ )
54 50 53 44 45 rlim3 ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝐶 ) ) < 𝑦 ) ) )
55 39 46 54 3bitr4d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 ) )
56 55 ex ⊢ ( 𝜑 → ( 𝐶 ∈ ℂ → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 ) ) )
57 5 7 56 pm5.21ndd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 ) )
58 1 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
59 58 breq1d ⊢ ( 𝜑 → ( 𝐹 ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 ) )
60 resres ⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ ( 𝐵 [,) +∞ ) ) = ( 𝐹 ↾ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) )
61 ffn ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → 𝐹 Fn 𝐴 )
62 fnresdm ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
63 1 61 62 3syl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
64 63 reseq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) ↾ ( 𝐵 [,) +∞ ) ) = ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) )
65 58 reseq1d ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ) )
66 resmpt ⊢ ( ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
67 51 66 ax-mp ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) )
68 65 67 eqtrdi ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
69 60 64 68 3eqtr3a ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
70 69 breq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐶 ) )
71 57 59 70 3bitr4d ⊢ ( 𝜑 → ( 𝐹 ⇝𝑟 𝐶 ↔ ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ⇝𝑟 𝐶 ) )