MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lo1res Structured version   Visualization version   GIF version

Theorem lo1res 14485
Description: The restriction of an eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 15-Sep-2014.)
Assertion
Ref Expression
lo1res (𝐹 ∈ ≤𝑂(1) → (𝐹𝐴) ∈ ≤𝑂(1))

Proof of Theorem lo1res
Dummy variables 𝑥 𝑚 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lo1f 14444 . . . 4 (𝐹 ∈ ≤𝑂(1) → 𝐹:dom 𝐹⟶ℝ)
2 lo1bdd 14446 . . . 4 ((𝐹 ∈ ≤𝑂(1) ∧ 𝐹:dom 𝐹⟶ℝ) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ dom 𝐹(𝑥𝑦 → (𝐹𝑦) ≤ 𝑚))
31, 2mpdan 705 . . 3 (𝐹 ∈ ≤𝑂(1) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ dom 𝐹(𝑥𝑦 → (𝐹𝑦) ≤ 𝑚))
4 inss1 3972 . . . . . . 7 (dom 𝐹𝐴) ⊆ dom 𝐹
5 ssralv 3803 . . . . . . 7 ((dom 𝐹𝐴) ⊆ dom 𝐹 → (∀𝑦 ∈ dom 𝐹(𝑥𝑦 → (𝐹𝑦) ≤ 𝑚) → ∀𝑦 ∈ (dom 𝐹𝐴)(𝑥𝑦 → (𝐹𝑦) ≤ 𝑚)))
64, 5ax-mp 5 . . . . . 6 (∀𝑦 ∈ dom 𝐹(𝑥𝑦 → (𝐹𝑦) ≤ 𝑚) → ∀𝑦 ∈ (dom 𝐹𝐴)(𝑥𝑦 → (𝐹𝑦) ≤ 𝑚))
7 inss2 3973 . . . . . . . . . . 11 (dom 𝐹𝐴) ⊆ 𝐴
87sseli 3736 . . . . . . . . . 10 (𝑦 ∈ (dom 𝐹𝐴) → 𝑦𝐴)
9 fvres 6364 . . . . . . . . . 10 (𝑦𝐴 → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
108, 9syl 17 . . . . . . . . 9 (𝑦 ∈ (dom 𝐹𝐴) → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
1110breq1d 4810 . . . . . . . 8 (𝑦 ∈ (dom 𝐹𝐴) → (((𝐹𝐴)‘𝑦) ≤ 𝑚 ↔ (𝐹𝑦) ≤ 𝑚))
1211imbi2d 329 . . . . . . 7 (𝑦 ∈ (dom 𝐹𝐴) → ((𝑥𝑦 → ((𝐹𝐴)‘𝑦) ≤ 𝑚) ↔ (𝑥𝑦 → (𝐹𝑦) ≤ 𝑚)))
1312ralbiia 3113 . . . . . 6 (∀𝑦 ∈ (dom 𝐹𝐴)(𝑥𝑦 → ((𝐹𝐴)‘𝑦) ≤ 𝑚) ↔ ∀𝑦 ∈ (dom 𝐹𝐴)(𝑥𝑦 → (𝐹𝑦) ≤ 𝑚))
146, 13sylibr 224 . . . . 5 (∀𝑦 ∈ dom 𝐹(𝑥𝑦 → (𝐹𝑦) ≤ 𝑚) → ∀𝑦 ∈ (dom 𝐹𝐴)(𝑥𝑦 → ((𝐹𝐴)‘𝑦) ≤ 𝑚))
1514reximi 3145 . . . 4 (∃𝑚 ∈ ℝ ∀𝑦 ∈ dom 𝐹(𝑥𝑦 → (𝐹𝑦) ≤ 𝑚) → ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹𝐴)(𝑥𝑦 → ((𝐹𝐴)‘𝑦) ≤ 𝑚))
1615reximi 3145 . . 3 (∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ dom 𝐹(𝑥𝑦 → (𝐹𝑦) ≤ 𝑚) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹𝐴)(𝑥𝑦 → ((𝐹𝐴)‘𝑦) ≤ 𝑚))
173, 16syl 17 . 2 (𝐹 ∈ ≤𝑂(1) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹𝐴)(𝑥𝑦 → ((𝐹𝐴)‘𝑦) ≤ 𝑚))
18 fssres 6227 . . . . 5 ((𝐹:dom 𝐹⟶ℝ ∧ (dom 𝐹𝐴) ⊆ dom 𝐹) → (𝐹 ↾ (dom 𝐹𝐴)):(dom 𝐹𝐴)⟶ℝ)
191, 4, 18sylancl 697 . . . 4 (𝐹 ∈ ≤𝑂(1) → (𝐹 ↾ (dom 𝐹𝐴)):(dom 𝐹𝐴)⟶ℝ)
20 resres 5563 . . . . . 6 ((𝐹 ↾ dom 𝐹) ↾ 𝐴) = (𝐹 ↾ (dom 𝐹𝐴))
21 ffn 6202 . . . . . . . 8 (𝐹:dom 𝐹⟶ℝ → 𝐹 Fn dom 𝐹)
22 fnresdm 6157 . . . . . . . 8 (𝐹 Fn dom 𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹)
231, 21, 223syl 18 . . . . . . 7 (𝐹 ∈ ≤𝑂(1) → (𝐹 ↾ dom 𝐹) = 𝐹)
2423reseq1d 5546 . . . . . 6 (𝐹 ∈ ≤𝑂(1) → ((𝐹 ↾ dom 𝐹) ↾ 𝐴) = (𝐹𝐴))
2520, 24syl5eqr 2804 . . . . 5 (𝐹 ∈ ≤𝑂(1) → (𝐹 ↾ (dom 𝐹𝐴)) = (𝐹𝐴))
2625feq1d 6187 . . . 4 (𝐹 ∈ ≤𝑂(1) → ((𝐹 ↾ (dom 𝐹𝐴)):(dom 𝐹𝐴)⟶ℝ ↔ (𝐹𝐴):(dom 𝐹𝐴)⟶ℝ))
2719, 26mpbid 222 . . 3 (𝐹 ∈ ≤𝑂(1) → (𝐹𝐴):(dom 𝐹𝐴)⟶ℝ)
28 lo1dm 14445 . . . 4 (𝐹 ∈ ≤𝑂(1) → dom 𝐹 ⊆ ℝ)
294, 28syl5ss 3751 . . 3 (𝐹 ∈ ≤𝑂(1) → (dom 𝐹𝐴) ⊆ ℝ)
30 ello12 14442 . . 3 (((𝐹𝐴):(dom 𝐹𝐴)⟶ℝ ∧ (dom 𝐹𝐴) ⊆ ℝ) → ((𝐹𝐴) ∈ ≤𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹𝐴)(𝑥𝑦 → ((𝐹𝐴)‘𝑦) ≤ 𝑚)))
3127, 29, 30syl2anc 696 . 2 (𝐹 ∈ ≤𝑂(1) → ((𝐹𝐴) ∈ ≤𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹𝐴)(𝑥𝑦 → ((𝐹𝐴)‘𝑦) ≤ 𝑚)))
3217, 31mpbird 247 1 (𝐹 ∈ ≤𝑂(1) → (𝐹𝐴) ∈ ≤𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1628  wcel 2135  wral 3046  wrex 3047  cin 3710  wss 3711   class class class wbr 4800  dom cdm 5262  cres 5264   Fn wfn 6040  wf 6041  cfv 6045  cr 10123  cle 10263  ≤𝑂(1)clo1 14413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-cnex 10180  ax-resscn 10181  ax-pre-lttri 10198  ax-pre-lttrn 10199
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-po 5183  df-so 5184  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-er 7907  df-pm 8022  df-en 8118  df-dom 8119  df-sdom 8120  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-ico 12370  df-lo1 14417
This theorem is referenced by:  o1res  14486  lo1res2  14488  lo1resb  14490
  Copyright terms: Public domain W3C validator