Step |
Hyp |
Ref |
Expression |
1 |
|
lo1o12.1 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) |
2 |
1
|
fmpttd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ ) |
3 |
|
lo1o1 |
⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( abs ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ≤𝑂(1) ) ) |
4 |
2 3
|
syl |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( abs ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ≤𝑂(1) ) ) |
5 |
|
absf |
⊢ abs : ℂ ⟶ ℝ |
6 |
5
|
a1i |
⊢ ( 𝜑 → abs : ℂ ⟶ ℝ ) |
7 |
6 1
|
cofmpt |
⊢ ( 𝜑 → ( abs ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ) |
8 |
7
|
eleq1d |
⊢ ( 𝜑 → ( ( abs ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ≤𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ) ) |
9 |
4 8
|
bitrd |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ) ) |