Metamath Proof Explorer

Theorem o1co

Description: Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses o1co.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
o1co.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝑂(1) )
o1co.3 ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
o1co.4 ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
o1co.5 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) ) )
Assertion o1co ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 o1co.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 o1co.2 ⊢ ( 𝜑 → 𝐹 ∈ 𝑂(1) )
3 o1co.3 ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
4 o1co.4 ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
5 o1co.5 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) ) )
6 1 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
7 o1dm ⊢ ( 𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ )
8 2 7 syl ⊢ ( 𝜑 → dom 𝐹 ⊆ ℝ )
9 6 8 eqsstrrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
10 elo12 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑚 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) )
11 1 9 10 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑚 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) )
12 2 11 mpbid ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) )
13 reeanv ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℝ ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) ) ∧ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) )
14 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) → 𝐺 : 𝐵 ⟶ 𝐴 )
15 14 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 )
16 breq2 ⊢ ( 𝑧 = ( 𝐺 ‘ 𝑦 ) → ( 𝑚 ≤ 𝑧 ↔ 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) ) )
17 2fveq3 ⊢ ( 𝑧 = ( 𝐺 ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
18 17 breq1d ⊢ ( 𝑧 = ( 𝐺 ‘ 𝑦 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ↔ ( abs ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ≤ 𝑛 ) )
19 16 18 imbi12d ⊢ ( 𝑧 = ( 𝐺 ‘ 𝑦 ) → ( ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ↔ ( 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ≤ 𝑛 ) ) )
20 19 rspcva ⊢ ( ( ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ≤ 𝑛 ) )
21 15 20 sylan ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) ∧ 𝑦 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ≤ 𝑛 ) )
22 21 an32s ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ≤ 𝑛 ) )
23 14 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → 𝐺 : 𝐵 ⟶ 𝐴 )
24 fvco3 ⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
25 23 24 sylan ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
26 25 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
27 26 breq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ↔ ( abs ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ≤ 𝑛 ) )
28 22 27 sylibrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) )
29 28 imim2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 → 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) ) → ( 𝑥 ≤ 𝑦 → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) ) )
30 29 ralimdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) ) )
31 30 expimpd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) → ( ( ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) ) ) → ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) ) )
32 31 ancomsd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ ℝ ) → ( ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) ) )
33 32 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑛 ∈ ℝ ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ∃ 𝑛 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) ) )
34 33 reximdva ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℝ ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) ) )
35 13 34 biimtrrid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → ( ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ ( 𝐺 ‘ 𝑦 ) ) ∧ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) ) → ∃ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) ) )
36 5 35 mpand ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → ( ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) ) )
37 36 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ≤ 𝑧 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑛 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) ) )
38 12 37 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) )
39 fco ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) → ( 𝐹 ∘ 𝐺 ) : 𝐵 ⟶ ℂ )
40 1 3 39 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝐵 ⟶ ℂ )
41 elo12 ⊢ ( ( ( 𝐹 ∘ 𝐺 ) : 𝐵 ⟶ ℂ ∧ 𝐵 ⊆ ℝ ) → ( ( 𝐹 ∘ 𝐺 ) ∈ 𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) ) )
42 40 4 41 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) ∈ 𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑛 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ≤ 𝑛 ) ) )
43 38 42 mpbird ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) ∈ 𝑂(1) )