Metamath Proof Explorer


Theorem elo12

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

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

Proof

Step Hyp Ref Expression
1 cnex ℂ ∈ V
2 reex ℝ ∈ V
3 elpm2r ( ( ( ℂ ∈ V ∧ ℝ ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
4 1 2 3 mpanl12 ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
5 elo1 ( 𝐹 ∈ 𝑂(1) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) )
6 5 baib ( 𝐹 ∈ ( ℂ ↑pm ℝ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) )
7 4 6 syl ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) )
8 elin ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦 ∈ dom 𝐹𝑦 ∈ ( 𝑥 [,) +∞ ) ) )
9 fdm ( 𝐹 : 𝐴 ⟶ ℂ → dom 𝐹 = 𝐴 )
10 9 ad3antrrr ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → dom 𝐹 = 𝐴 )
11 10 eleq2d ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( 𝑦 ∈ dom 𝐹𝑦𝐴 ) )
12 11 anbi1d ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ dom 𝐹𝑦 ∈ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦𝐴𝑦 ∈ ( 𝑥 [,) +∞ ) ) ) )
13 simpllr ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → 𝐴 ⊆ ℝ )
14 13 sselda ( ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦𝐴 ) → 𝑦 ∈ ℝ )
15 simpllr ( ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦𝐴 ) → 𝑥 ∈ ℝ )
16 elicopnf ( 𝑥 ∈ ℝ → ( 𝑦 ∈ ( 𝑥 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥𝑦 ) ) )
17 15 16 syl ( ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦𝐴 ) → ( 𝑦 ∈ ( 𝑥 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥𝑦 ) ) )
18 14 17 mpbirand ( ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦𝐴 ) → ( 𝑦 ∈ ( 𝑥 [,) +∞ ) ↔ 𝑥𝑦 ) )
19 18 pm5.32da ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦𝐴𝑦 ∈ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦𝐴𝑥𝑦 ) ) )
20 12 19 bitrd ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ dom 𝐹𝑦 ∈ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦𝐴𝑥𝑦 ) ) )
21 8 20 syl5bb ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦𝐴𝑥𝑦 ) ) )
22 21 imbi1d ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) ↔ ( ( 𝑦𝐴𝑥𝑦 ) → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) ) )
23 impexp ( ( ( 𝑦𝐴𝑥𝑦 ) → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) ↔ ( 𝑦𝐴 → ( 𝑥𝑦 → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) ) )
24 22 23 bitrdi ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) ↔ ( 𝑦𝐴 → ( 𝑥𝑦 → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) ) ) )
25 24 ralbidv2 ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ↔ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) ) )
26 25 rexbidva ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ↔ ∃ 𝑚 ∈ ℝ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) ) )
27 26 rexbidva ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) ) )
28 7 27 bitrd ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) ) )