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

Theorem elo1 15468
Description: Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.)
Assertion
Ref Expression
elo1 (𝐹 ∈ 𝑂(1) ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹𝑦)) ≤ 𝑚))
Distinct variable group:   𝑥,𝑚,𝑦,𝐹

Proof of Theorem elo1
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 dmeq 5894 . . . . 5 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
21ineq1d 4204 . . . 4 (𝑓 = 𝐹 → (dom 𝑓 ∩ (𝑥[,)+∞)) = (dom 𝐹 ∩ (𝑥[,)+∞)))
3 fveq1 6881 . . . . . 6 (𝑓 = 𝐹 → (𝑓𝑦) = (𝐹𝑦))
43fveq2d 6886 . . . . 5 (𝑓 = 𝐹 → (abs‘(𝑓𝑦)) = (abs‘(𝐹𝑦)))
54breq1d 5149 . . . 4 (𝑓 = 𝐹 → ((abs‘(𝑓𝑦)) ≤ 𝑚 ↔ (abs‘(𝐹𝑦)) ≤ 𝑚))
62, 5raleqbidv 3334 . . 3 (𝑓 = 𝐹 → (∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓𝑦)) ≤ 𝑚 ↔ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹𝑦)) ≤ 𝑚))
762rexbidv 3211 . 2 (𝑓 = 𝐹 → (∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓𝑦)) ≤ 𝑚 ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹𝑦)) ≤ 𝑚))
8 df-o1 15432 . 2 𝑂(1) = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓𝑦)) ≤ 𝑚}
97, 8elrab2 3679 1 (𝐹 ∈ 𝑂(1) ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹𝑦)) ≤ 𝑚))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 395   = wceq 1533  wcel 2098  wral 3053  wrex 3062  cin 3940   class class class wbr 5139  dom cdm 5667  cfv 6534  (class class class)co 7402  pm cpm 8818  cc 11105  cr 11106  +∞cpnf 11243  cle 11247  [,)cico 13324  abscabs 15179  𝑂(1)co1 15428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-dm 5677  df-iota 6486  df-fv 6542  df-o1 15432
This theorem is referenced by:  elo12  15469  o1f  15471  o1dm  15472
  Copyright terms: Public domain W3C validator