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 ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) )