This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 → 𝑚 ≤ ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ 𝐶 ) ) )
27 26 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 → 𝑚 ≤ ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ 𝐶 ) ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 → 𝑚 ≤ ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑚 ≤ 𝐶 ) ) )
29 5 28 mpbird ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 → 𝑚 ≤ ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑧 ) ) )
30 1 2 6 4 29 o1co ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ) ∈ 𝑂(1) )