Metamath Proof Explorer


Theorem o1compt

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

Ref Expression
Hypotheses o1compt.1 ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
o1compt.2 ( 𝜑𝐹 ∈ 𝑂(1) )
o1compt.3 ( ( 𝜑𝑦𝐵 ) → 𝐶𝐴 )
o1compt.4 ( 𝜑𝐵 ⊆ ℝ )
o1compt.5 ( ( 𝜑𝑚 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 ( 𝑥𝑦𝑚𝐶 ) )
Assertion o1compt ( 𝜑 → ( 𝐹 ∘ ( 𝑦𝐵𝐶 ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 o1compt.1 ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
2 o1compt.2 ( 𝜑𝐹 ∈ 𝑂(1) )
3 o1compt.3 ( ( 𝜑𝑦𝐵 ) → 𝐶𝐴 )
4 o1compt.4 ( 𝜑𝐵 ⊆ ℝ )
5 o1compt.5 ( ( 𝜑𝑚 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 ( 𝑥𝑦𝑚𝐶 ) )
6 3 fmpttd ( 𝜑 → ( 𝑦𝐵𝐶 ) : 𝐵𝐴 )
7 nfv 𝑦 𝑥𝑧
8 nfcv 𝑦 𝑚
9 nfcv 𝑦
10 nffvmpt1 𝑦 ( ( 𝑦𝐵𝐶 ) ‘ 𝑧 )
11 8 9 10 nfbr 𝑦 𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑧 )
12 7 11 nfim 𝑦 ( 𝑥𝑧𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑧 ) )
13 nfv 𝑧 ( 𝑥𝑦𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑦 ) )
14 breq2 ( 𝑧 = 𝑦 → ( 𝑥𝑧𝑥𝑦 ) )
15 fveq2 ( 𝑧 = 𝑦 → ( ( 𝑦𝐵𝐶 ) ‘ 𝑧 ) = ( ( 𝑦𝐵𝐶 ) ‘ 𝑦 ) )
16 15 breq2d ( 𝑧 = 𝑦 → ( 𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑧 ) ↔ 𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑦 ) ) )
17 14 16 imbi12d ( 𝑧 = 𝑦 → ( ( 𝑥𝑧𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑧 ) ) ↔ ( 𝑥𝑦𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑦 ) ) ) )
18 12 13 17 cbvralw ( ∀ 𝑧𝐵 ( 𝑥𝑧𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑧 ) ) ↔ ∀ 𝑦𝐵 ( 𝑥𝑦𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑦 ) ) )
19 simpr ( ( 𝜑𝑦𝐵 ) → 𝑦𝐵 )
20 eqid ( 𝑦𝐵𝐶 ) = ( 𝑦𝐵𝐶 )
21 20 fvmpt2 ( ( 𝑦𝐵𝐶𝐴 ) → ( ( 𝑦𝐵𝐶 ) ‘ 𝑦 ) = 𝐶 )
22 19 3 21 syl2anc ( ( 𝜑𝑦𝐵 ) → ( ( 𝑦𝐵𝐶 ) ‘ 𝑦 ) = 𝐶 )
23 22 breq2d ( ( 𝜑𝑦𝐵 ) → ( 𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑦 ) ↔ 𝑚𝐶 ) )
24 23 imbi2d ( ( 𝜑𝑦𝐵 ) → ( ( 𝑥𝑦𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑦 ) ) ↔ ( 𝑥𝑦𝑚𝐶 ) ) )
25 24 ralbidva ( 𝜑 → ( ∀ 𝑦𝐵 ( 𝑥𝑦𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑦 ) ) ↔ ∀ 𝑦𝐵 ( 𝑥𝑦𝑚𝐶 ) ) )
26 18 25 syl5bb ( 𝜑 → ( ∀ 𝑧𝐵 ( 𝑥𝑧𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑧 ) ) ↔ ∀ 𝑦𝐵 ( 𝑥𝑦𝑚𝐶 ) ) )
27 26 rexbidv ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧𝐵 ( 𝑥𝑧𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 ( 𝑥𝑦𝑚𝐶 ) ) )
28 27 adantr ( ( 𝜑𝑚 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧𝐵 ( 𝑥𝑧𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 ( 𝑥𝑦𝑚𝐶 ) ) )
29 5 28 mpbird ( ( 𝜑𝑚 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧𝐵 ( 𝑥𝑧𝑚 ≤ ( ( 𝑦𝐵𝐶 ) ‘ 𝑧 ) ) )
30 1 2 6 4 29 o1co ( 𝜑 → ( 𝐹 ∘ ( 𝑦𝐵𝐶 ) ) ∈ 𝑂(1) )