Step | Hyp | Ref
| Expression |
1 | | o1co.2 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝑂(1)) |
2 | | o1co.1 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
3 | 2 | fdmd 6516 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = 𝐴) |
4 | | o1dm 14980 |
. . . . . . 7
⊢ (𝐹 ∈ 𝑂(1) → dom
𝐹 ⊆
ℝ) |
5 | 1, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 ⊆ ℝ) |
6 | 3, 5 | eqsstrrd 3917 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
7 | | elo12 14977 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → (𝐹 ∈ 𝑂(1) ↔ ∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛))) |
8 | 2, 6, 7 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝐹 ∈ 𝑂(1) ↔ ∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛))) |
9 | 1, 8 | mpbid 235 |
. . 3
⊢ (𝜑 → ∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) |
10 | | o1co.5 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ (𝐺‘𝑦))) |
11 | | reeanv 3271 |
. . . . . 6
⊢
(∃𝑥 ∈
ℝ ∃𝑛 ∈
ℝ (∀𝑦 ∈
𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ (𝐺‘𝑦)) ∧ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) ↔ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ (𝐺‘𝑦)) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛))) |
12 | | o1co.3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
13 | 12 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) → 𝐺:𝐵⟶𝐴) |
14 | 13 | ffvelrnda 6864 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) ∧ 𝑦 ∈ 𝐵) → (𝐺‘𝑦) ∈ 𝐴) |
15 | | breq2 5035 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝐺‘𝑦) → (𝑚 ≤ 𝑧 ↔ 𝑚 ≤ (𝐺‘𝑦))) |
16 | | 2fveq3 6682 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝐺‘𝑦) → (abs‘(𝐹‘𝑧)) = (abs‘(𝐹‘(𝐺‘𝑦)))) |
17 | 16 | breq1d 5041 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝐺‘𝑦) → ((abs‘(𝐹‘𝑧)) ≤ 𝑛 ↔ (abs‘(𝐹‘(𝐺‘𝑦))) ≤ 𝑛)) |
18 | 15, 17 | imbi12d 348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐺‘𝑦) → ((𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛) ↔ (𝑚 ≤ (𝐺‘𝑦) → (abs‘(𝐹‘(𝐺‘𝑦))) ≤ 𝑛))) |
19 | 18 | rspcva 3525 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺‘𝑦) ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) → (𝑚 ≤ (𝐺‘𝑦) → (abs‘(𝐹‘(𝐺‘𝑦))) ≤ 𝑛)) |
20 | 14, 19 | sylan 583 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) → (𝑚 ≤ (𝐺‘𝑦) → (abs‘(𝐹‘(𝐺‘𝑦))) ≤ 𝑛)) |
21 | 20 | an32s 652 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) ∧
∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) ∧ 𝑦 ∈ 𝐵) → (𝑚 ≤ (𝐺‘𝑦) → (abs‘(𝐹‘(𝐺‘𝑦))) ≤ 𝑛)) |
22 | 13 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) ∧
∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) → 𝐺:𝐵⟶𝐴) |
23 | | fvco3 6770 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:𝐵⟶𝐴 ∧ 𝑦 ∈ 𝐵) → ((𝐹 ∘ 𝐺)‘𝑦) = (𝐹‘(𝐺‘𝑦))) |
24 | 22, 23 | sylan 583 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) ∧
∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) ∧ 𝑦 ∈ 𝐵) → ((𝐹 ∘ 𝐺)‘𝑦) = (𝐹‘(𝐺‘𝑦))) |
25 | 24 | fveq2d 6681 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) ∧
∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) ∧ 𝑦 ∈ 𝐵) → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) = (abs‘(𝐹‘(𝐺‘𝑦)))) |
26 | 25 | breq1d 5041 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) ∧
∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) ∧ 𝑦 ∈ 𝐵) → ((abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛 ↔ (abs‘(𝐹‘(𝐺‘𝑦))) ≤ 𝑛)) |
27 | 21, 26 | sylibrd 262 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) ∧
∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) ∧ 𝑦 ∈ 𝐵) → (𝑚 ≤ (𝐺‘𝑦) → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛)) |
28 | 27 | imim2d 57 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) ∧
∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 → 𝑚 ≤ (𝐺‘𝑦)) → (𝑥 ≤ 𝑦 → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛))) |
29 | 28 | ralimdva 3092 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) ∧
∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) → (∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ (𝐺‘𝑦)) → ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛))) |
30 | 29 | expimpd 457 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) → ((∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛) ∧ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ (𝐺‘𝑦))) → ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛))) |
31 | 30 | ancomsd 469 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ 𝑛 ∈ ℝ) → ((∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ (𝐺‘𝑦)) ∧ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) → ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛))) |
32 | 31 | reximdva 3185 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (∃𝑛 ∈ ℝ (∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ (𝐺‘𝑦)) ∧ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) → ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛))) |
33 | 32 | reximdva 3185 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → (∃𝑥 ∈ ℝ ∃𝑛 ∈ ℝ (∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ (𝐺‘𝑦)) ∧ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) → ∃𝑥 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛))) |
34 | 11, 33 | syl5bir 246 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → ((∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑚 ≤ (𝐺‘𝑦)) ∧ ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛)) → ∃𝑥 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛))) |
35 | 10, 34 | mpand 695 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → (∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛) → ∃𝑥 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛))) |
36 | 35 | rexlimdva 3195 |
. . 3
⊢ (𝜑 → (∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑚 ≤ 𝑧 → (abs‘(𝐹‘𝑧)) ≤ 𝑛) → ∃𝑥 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛))) |
37 | 9, 36 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛)) |
38 | | fco 6529 |
. . . 4
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐵⟶𝐴) → (𝐹 ∘ 𝐺):𝐵⟶ℂ) |
39 | 2, 12, 38 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐵⟶ℂ) |
40 | | o1co.4 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
41 | | elo12 14977 |
. . 3
⊢ (((𝐹 ∘ 𝐺):𝐵⟶ℂ ∧ 𝐵 ⊆ ℝ) → ((𝐹 ∘ 𝐺) ∈ 𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛))) |
42 | 39, 40, 41 | syl2anc 587 |
. 2
⊢ (𝜑 → ((𝐹 ∘ 𝐺) ∈ 𝑂(1) ↔ ∃𝑥 ∈ ℝ ∃𝑛 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (abs‘((𝐹 ∘ 𝐺)‘𝑦)) ≤ 𝑛))) |
43 | 37, 42 | mpbird 260 |
1
⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ 𝑂(1)) |