Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐹 ∈ 𝑂(1) ) |
2 |
|
simpr |
⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ ) |
3 |
|
fdm |
⊢ ( 𝐹 : 𝐴 ⟶ ℂ → dom 𝐹 = 𝐴 ) |
4 |
3
|
adantl |
⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → dom 𝐹 = 𝐴 ) |
5 |
|
o1dm |
⊢ ( 𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ ) |
6 |
5
|
adantr |
⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → dom 𝐹 ⊆ ℝ ) |
7 |
4 6
|
eqsstrrd |
⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐴 ⊆ ℝ ) |
8 |
|
elo12 |
⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) ) |
9 |
2 7 8
|
syl2anc |
⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) ) |
10 |
1 9
|
mpbid |
⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) |