Theorem ello1 15076

Description: Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.)

Assertion

Ref	Expression
ello1	⊢ (𝐹 ∈ ≤𝑂(1) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚))

Distinct variable group:   𝑥,𝑚,𝑦,𝐹

Proof of Theorem ello1

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmeq 5772	. . . . 5 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
2	1	ineq1d 4126	. . . 4 ⊢ (𝑓 = 𝐹 → (dom 𝑓 ∩ (𝑥[,)+∞)) = (dom 𝐹 ∩ (𝑥[,)+∞)))
3		fveq1 6716	. . . . 5 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑦) = (𝐹‘𝑦))
4	3	breq1d 5063	. . . 4 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑦) ≤ 𝑚 ↔ (𝐹‘𝑦) ≤ 𝑚))
5	2, 4	raleqbidv 3313	. . 3 ⊢ (𝑓 = 𝐹 → (∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚 ↔ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚))
6	5	2rexbidv 3219	. 2 ⊢ (𝑓 = 𝐹 → (∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚 ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚))
7		df-lo1 15052	. 2 ⊢ ≤𝑂(1) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚}
8	6, 7	elrab2 3605	1 ⊢ (𝐹 ∈ ≤𝑂(1) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ 𝑚))

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2110  ∀wral 3061  ∃wrex 3062   ∩ cin 3865   class class class wbr 5053  dom cdm 5551  ‘cfv 6380  (class class class)co 7213   ↑_pm cpm 8509  ℝcr 10728  +∞cpnf 10864   ≤ cle 10868  [,)cico 12937  ≤𝑂(1)clo1 15048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-dm 5561  df-iota 6338  df-fv 6388  df-lo1 15052

This theorem is referenced by:  ello12  15077  lo1f  15079  lo1dm  15080