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 14057

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 14054	. . 3 ⊢ (𝐹 ∈ 𝑂(1) ↔ (𝐹 ∈ (ℂ ↑_pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(abs‘(𝐹‘𝑦)) ≤ 𝑚))
2	1	simplbi 474	. 2 ⊢ (𝐹 ∈ 𝑂(1) → 𝐹 ∈ (ℂ ↑_pm ℝ))
3		cnex 9874	. . . 4 ⊢ ℂ ∈ V
4		reex 9884	. . . 4 ⊢ ℝ ∈ V
5	3, 4	elpm2 7753	. . 3 ⊢ (𝐹 ∈ (ℂ ↑_pm ℝ) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
6	5	simplbi 474	. 2 ⊢ (𝐹 ∈ (ℂ ↑_pm ℝ) → 𝐹:dom 𝐹⟶ℂ)
7	2, 6	syl 17	1 ⊢ (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 1976 ∀wral 2895 ∃wrex 2896 ∩ cin 3538 ⊆ wss 3539 class class class wbr 4577 dom cdm 5028 ⟶wf 5786 ‘cfv 5790 (class class class)co 6527 ↑_pm cpm 7723 ℂcc 9791 ℝcr 9792 +∞cpnf 9928 ≤ cle 9932 [,)cico 12007 abscabs 13771 𝑂(1)co1 14014

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1712 ax-4 1727 ax-5 1826 ax-6 1874 ax-7 1921 ax-8 1978 ax-9 1985 ax-10 2005 ax-11 2020 ax-12 2033 ax-13 2233 ax-ext 2589 ax-sep 4703 ax-nul 4712 ax-pow 4764 ax-pr 4828 ax-un 6825 ax-cnex 9849 ax-resscn 9850

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3an 1032 df-tru 1477 df-ex 1695 df-nf 1700 df-sb 1867 df-eu 2461 df-mo 2462 df-clab 2596 df-cleq 2602 df-clel 2605 df-nfc 2739 df-ne 2781 df-ral 2900 df-rex 2901 df-rab 2904 df-v 3174 df-sbc 3402 df-dif 3542 df-un 3544 df-in 3546 df-ss 3553 df-nul 3874 df-if 4036 df-pw 4109 df-sn 4125 df-pr 4127 df-op 4131 df-uni 4367 df-br 4578 df-opab 4638 df-id 4943 df-xp 5034 df-rel 5035 df-cnv 5036 df-co 5037 df-dm 5038 df-rn 5039 df-iota 5754 df-fun 5792 df-fn 5793 df-f 5794 df-fv 5798 df-ov 6530 df-oprab 6531 df-mpt2 6532 df-pm 7725 df-o1 14018

This theorem is referenced by: o1res 14088 o1of2 14140 o1rlimmul 14146 o1mptrcl 14150 o1fsum 14335 o1cxp 24446 dchrisum0 24954

W3C validator