Theorem elo12 15436

Description: Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.)

Assertion

Ref	Expression
elo12	⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ 𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚)))

Distinct variable groups:   𝑥,𝑚,𝑦,𝐴   𝑚,𝐹,𝑥,𝑦

Proof of Theorem elo12

Step	Hyp	Ref	Expression
1		cnex 11094	. . . 4 ⊢ ℂ ∈ V
2		reex 11104	. . . 4 ⊢ ℝ ∈ V
3		elpm2r 8775	. . . 4 ⊢ (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm ℝ))
4	1, 2, 3	mpanl12 702	. . 3 ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → 𝐹 ∈ (ℂ ↑pm ℝ))
5		elo1 15435	. . . 4 ⊢ (𝐹 ∈ 𝑂(1) ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹‘𝑦)) ≤ 𝑚))
6	5	baib 535	. . 3 ⊢ (𝐹 ∈ (ℂ ↑pm ℝ) → (𝐹 ∈ 𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹‘𝑦)) ≤ 𝑚))
7	4, 6	syl 17	. 2 ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ 𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹‘𝑦)) ≤ 𝑚))
8		elin 3914	. . . . . . . 8 ⊢ (𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞)) ↔ (𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ (𝑥[,)+∞)))
9		fdm 6665	. . . . . . . . . . . 12 ⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴)
10	9	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → dom 𝐹 = 𝐴)
11	10	eleq2d 2819	. . . . . . . . . 10 ⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴))
12	11	anbi1d 631	. . . . . . . . 9 ⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ (𝑥[,)+∞)) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ (𝑥[,)+∞))))
13		simpllr 775	. . . . . . . . . . . 12 ⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → 𝐴 ⊆ ℝ)
14	13	sselda 3930	. . . . . . . . . . 11 ⊢ (((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
15		simpllr 775	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ ℝ)
16		elicopnf 13347	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑦 ∈ (𝑥[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦)))
17	15, 16	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ (𝑥[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦)))
18	14, 17	mpbirand 707	. . . . . . . . . 10 ⊢ (((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ (𝑥[,)+∞) ↔ 𝑥 ≤ 𝑦))
19	18	pm5.32da 579	. . . . . . . . 9 ⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ (𝑥[,)+∞)) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)))
20	12, 19	bitrd 279	. . . . . . . 8 ⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ (𝑥[,)+∞)) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)))
21	8, 20	bitrid 283	. . . . . . 7 ⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → (𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞)) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦)))
22	21	imbi1d 341	. . . . . 6 ⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞)) → (abs‘(𝐹‘𝑦)) ≤ 𝑚) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦) → (abs‘(𝐹‘𝑦)) ≤ 𝑚)))
23		impexp 450	. . . . . 6 ⊢ (((𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦) → (abs‘(𝐹‘𝑦)) ≤ 𝑚) ↔ (𝑦 ∈ 𝐴 → (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚)))
24	22, 23	bitrdi 287	. . . . 5 ⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → ((𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞)) → (abs‘(𝐹‘𝑦)) ≤ 𝑚) ↔ (𝑦 ∈ 𝐴 → (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚))))
25	24	ralbidv2 3152	. . . 4 ⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑚 ∈ ℝ) → (∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹‘𝑦)) ≤ 𝑚 ↔ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚)))
26	25	rexbidva 3155	. . 3 ⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹‘𝑦)) ≤ 𝑚 ↔ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚)))
27	26	rexbidva 3155	. 2 ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → (∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹‘𝑦)) ≤ 𝑚 ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚)))
28	7, 27	bitrd 279	1 ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ 𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (abs‘(𝐹‘𝑦)) ≤ 𝑚)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3048  ∃wrex 3057  Vcvv 3437   ∩ cin 3897   ⊆ wss 3898   class class class wbr 5093  dom cdm 5619  ⟶wf 6482  ‘cfv 6486  (class class class)co 7352   ↑_pm cpm 8757  ℂcc 11011  ℝcr 11012  +∞cpnf 11150   ≤ cle 11154  [,)cico 13249  abscabs 15143  𝑂(1)co1 15395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11069  ax-resscn 11070  ax-pre-lttri 11087  ax-pre-lttrn 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-er 8628  df-pm 8759  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-ico 13253  df-o1 15399

This theorem is referenced by:  elo12r  15437  o1bdd  15440  lo1o1  15441  o1co  15495  rlimo1  15526