Metamath Proof Explorer


Theorem lo1resb

Description: The restriction of a function to an unbounded-above interval is eventually upper bounded iff the original is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses lo1resb.1 ( 𝜑𝐹 : 𝐴 ⟶ ℝ )
lo1resb.2 ( 𝜑𝐴 ⊆ ℝ )
lo1resb.3 ( 𝜑𝐵 ∈ ℝ )
Assertion lo1resb ( 𝜑 → ( 𝐹 ∈ ≤𝑂(1) ↔ ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ∈ ≤𝑂(1) ) )

Proof

Step Hyp Ref Expression
1 lo1resb.1 ( 𝜑𝐹 : 𝐴 ⟶ ℝ )
2 lo1resb.2 ( 𝜑𝐴 ⊆ ℝ )
3 lo1resb.3 ( 𝜑𝐵 ∈ ℝ )
4 lo1res ( 𝐹 ∈ ≤𝑂(1) → ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ∈ ≤𝑂(1) )
5 1 feqmptd ( 𝜑𝐹 = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) )
6 5 reseq1d ( 𝜑 → ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) = ( ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) ↾ ( 𝐵 [,) +∞ ) ) )
7 resmpt3 ( ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) ↾ ( 𝐵 [,) +∞ ) ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹𝑥 ) )
8 6 7 eqtrdi ( 𝜑 → ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹𝑥 ) ) )
9 8 eleq1d ( 𝜑 → ( ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ∈ ≤𝑂(1) ↔ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹𝑥 ) ) ∈ ≤𝑂(1) ) )
10 inss1 ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ⊆ 𝐴
11 10 2 sstrid ( 𝜑 → ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ⊆ ℝ )
12 elinel1 ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) → 𝑥𝐴 )
13 ffvelrn ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ℝ )
14 1 12 13 syl2an ( ( 𝜑𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ) → ( 𝐹𝑥 ) ∈ ℝ )
15 11 14 ello1mpt ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹𝑥 ) ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) )
16 elin ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↔ ( 𝑥𝐴𝑥 ∈ ( 𝐵 [,) +∞ ) ) )
17 16 imbi1i ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) → ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) ↔ ( ( 𝑥𝐴𝑥 ∈ ( 𝐵 [,) +∞ ) ) → ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) )
18 impexp ( ( ( 𝑥𝐴𝑥 ∈ ( 𝐵 [,) +∞ ) ) → ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) ↔ ( 𝑥𝐴 → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) ) )
19 17 18 bitri ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) → ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) ↔ ( 𝑥𝐴 → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) ) )
20 impexp ( ( ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ∧ 𝑦𝑥 ) → ( 𝐹𝑥 ) ≤ 𝑧 ) ↔ ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) )
21 3 ad2antrr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℝ )
22 2 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → 𝐴 ⊆ ℝ )
23 22 sselda ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → 𝑥 ∈ ℝ )
24 elicopnf ( 𝐵 ∈ ℝ → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐵𝑥 ) ) )
25 24 baibd ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ↔ 𝐵𝑥 ) )
26 21 23 25 syl2anc ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ↔ 𝐵𝑥 ) )
27 26 anbi1d ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ∧ 𝑦𝑥 ) ↔ ( 𝐵𝑥𝑦𝑥 ) ) )
28 simplrl ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → 𝑦 ∈ ℝ )
29 maxle ( ( 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 ↔ ( 𝐵𝑥𝑦𝑥 ) ) )
30 21 28 23 29 syl3anc ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 ↔ ( 𝐵𝑥𝑦𝑥 ) ) )
31 27 30 bitr4d ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ∧ 𝑦𝑥 ) ↔ if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 ) )
32 31 imbi1d ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( ( ( 𝑥 ∈ ( 𝐵 [,) +∞ ) ∧ 𝑦𝑥 ) → ( 𝐹𝑥 ) ≤ 𝑧 ) ↔ ( if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) )
33 20 32 bitr3id ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) ∧ 𝑥𝐴 ) → ( ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) ↔ ( if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) )
34 33 pm5.74da ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( 𝑥𝐴 → ( 𝑥 ∈ ( 𝐵 [,) +∞ ) → ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) ) ↔ ( 𝑥𝐴 → ( if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) ) )
35 19 34 syl5bb ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) → ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) ↔ ( 𝑥𝐴 → ( if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) ) )
36 35 ralbidv2 ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ↔ ∀ 𝑥𝐴 ( if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) )
37 1 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → 𝐹 : 𝐴 ⟶ ℝ )
38 simprl ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → 𝑦 ∈ ℝ )
39 3 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
40 38 39 ifcld ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ∈ ℝ )
41 simprr ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → 𝑧 ∈ ℝ )
42 ello12r ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 ( if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) ) → 𝐹 ∈ ≤𝑂(1) )
43 42 3expia ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ ( if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ∀ 𝑥𝐴 ( if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) → 𝐹 ∈ ≤𝑂(1) ) )
44 37 22 40 41 43 syl22anc ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ∀ 𝑥𝐴 ( if ( 𝐵𝑦 , 𝑦 , 𝐵 ) ≤ 𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) → 𝐹 ∈ ≤𝑂(1) ) )
45 36 44 sylbid ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) → 𝐹 ∈ ≤𝑂(1) ) )
46 45 rexlimdvva ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ( 𝑦𝑥 → ( 𝐹𝑥 ) ≤ 𝑧 ) → 𝐹 ∈ ≤𝑂(1) ) )
47 15 46 sylbid ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 [,) +∞ ) ) ↦ ( 𝐹𝑥 ) ) ∈ ≤𝑂(1) → 𝐹 ∈ ≤𝑂(1) ) )
48 9 47 sylbid ( 𝜑 → ( ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ∈ ≤𝑂(1) → 𝐹 ∈ ≤𝑂(1) ) )
49 4 48 impbid2 ( 𝜑 → ( 𝐹 ∈ ≤𝑂(1) ↔ ( 𝐹 ↾ ( 𝐵 [,) +∞ ) ) ∈ ≤𝑂(1) ) )