Metamath Proof Explorer

Theorem lo1o1

Description: A function is eventually bounded iff its absolute value is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion lo1o1 ⊢F:A⟶ℂ→F∈𝑂⁡1↔abs∘F∈≤𝑂⁡1

Proof

Step Hyp Ref Expression
1 o1dm ⊢F∈𝑂⁡1→dom⁡F⊆ℝ
2 fdm ⊢F:A⟶ℂ→dom⁡F=A
3 2 sseq1d ⊢F:A⟶ℂ→dom⁡F⊆ℝ↔A⊆ℝ
4 1 3 imbitrid ⊢F:A⟶ℂ→F∈𝑂⁡1→A⊆ℝ
5 lo1dm ⊢abs∘F∈≤𝑂⁡1→dom⁡abs∘F⊆ℝ
6 absf ⊢abs:ℂ⟶ℝ
7 fco ⊢abs:ℂ⟶ℝ∧F:A⟶ℂ→abs∘F:A⟶ℝ
8 6 7 mpan ⊢F:A⟶ℂ→abs∘F:A⟶ℝ
9 8 fdmd ⊢F:A⟶ℂ→dom⁡abs∘F=A
10 9 sseq1d ⊢F:A⟶ℂ→dom⁡abs∘F⊆ℝ↔A⊆ℝ
11 5 10 imbitrid ⊢F:A⟶ℂ→abs∘F∈≤𝑂⁡1→A⊆ℝ
12 fvco3 ⊢F:A⟶ℂ∧y∈A→abs∘F⁡y=F⁡y
13 12 adantlr ⊢F:A⟶ℂ∧A⊆ℝ∧y∈A→abs∘F⁡y=F⁡y
14 13 breq1d ⊢F:A⟶ℂ∧A⊆ℝ∧y∈A→abs∘F⁡y≤m↔F⁡y≤m
15 14 imbi2d ⊢F:A⟶ℂ∧A⊆ℝ∧y∈A→x≤y→abs∘F⁡y≤m↔x≤y→F⁡y≤m
16 15 ralbidva ⊢F:A⟶ℂ∧A⊆ℝ→∀y∈Ax≤y→abs∘F⁡y≤m↔∀y∈Ax≤y→F⁡y≤m
17 16 2rexbidv ⊢F:A⟶ℂ∧A⊆ℝ→∃x∈ℝ∃m∈ℝ∀y∈Ax≤y→abs∘F⁡y≤m↔∃x∈ℝ∃m∈ℝ∀y∈Ax≤y→F⁡y≤m
18 ello12 ⊢abs∘F:A⟶ℝ∧A⊆ℝ→abs∘F∈≤𝑂⁡1↔∃x∈ℝ∃m∈ℝ∀y∈Ax≤y→abs∘F⁡y≤m
19 8 18 sylan ⊢F:A⟶ℂ∧A⊆ℝ→abs∘F∈≤𝑂⁡1↔∃x∈ℝ∃m∈ℝ∀y∈Ax≤y→abs∘F⁡y≤m
20 elo12 ⊢F:A⟶ℂ∧A⊆ℝ→F∈𝑂⁡1↔∃x∈ℝ∃m∈ℝ∀y∈Ax≤y→F⁡y≤m
21 17 19 20 3bitr4rd ⊢F:A⟶ℂ∧A⊆ℝ→F∈𝑂⁡1↔abs∘F∈≤𝑂⁡1
22 21 ex ⊢F:A⟶ℂ→A⊆ℝ→F∈𝑂⁡1↔abs∘F∈≤𝑂⁡1
23 4 11 22 pm5.21ndd ⊢F:A⟶ℂ→F∈𝑂⁡1↔abs∘F∈≤𝑂⁡1