o1f - Metamath Proof Explorer

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

Theorem o1f 15568

Description: An eventually bounded function is a function. (Contributed by Mario Carneiro, 15-Sep-2014.)

**Assertion**
Ref	Expression
o1f	⊢ (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ)

Proof of Theorem o1f Dummy variables 𝑥 𝑚 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elo1 15565	. . 3 ⊢ (𝐹 ∈ 𝑂(1) ↔ (𝐹 ∈ (ℂ ↑_pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹‘𝑦)) ≤ 𝑚))
2	1	simplbi 501	. 2 ⊢ (𝐹 ∈ 𝑂(1) → 𝐹 ∈ (ℂ ↑_pm ℝ))
3		cnex 11169	. . . 4 ⊢ ℂ ∈ V
4		reex 11179	. . . 4 ⊢ ℝ ∈ V
5	3, 4	elpm2 8860	. . 3 ⊢ (𝐹 ∈ (ℂ ↑_pm ℝ) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
6	5	simplbi 501	. 2 ⊢ (𝐹 ∈ (ℂ ↑_pm ℝ) → 𝐹:dom 𝐹⟶ℂ)
7	2, 6	syl 18	1 ⊢ (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2145 ∀wral 3079 ∃wrex 3089 ∩ cin 3906 ⊆ wss 3907 class class class wbr 5104 dom cdm 5651 ⟶wf 6521 ‘cfv 6525 (class class class)co 7400 ↑_pm cpm 8813 ℂcc 11086 ℝcr 11087 +∞cpnf 11228 ≤ cle 11232 [,)cico 13362 abscabs 15273 𝑂(1)co1 15525

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-cnex 11144 ax-resscn 11145

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-sbc 3748 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5105 df-opab 5167 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-pm 8815 df-o1 15529

This theorem is referenced by: o1res 15599 o1of2 15652 o1rlimmul 15658 o1mptrcl 15662 o1fsum 15853 o1cxp 27093 dchrisum0 27638

W3C validator