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 ⊢ φ → F : A ⟶ ℂ
o1compt.2 ⊢ φ → F ∈ 𝑂⁡1
o1compt.3 ⊢ φ ∧ y ∈ B → C ∈ A
o1compt.4 ⊢ φ → B ⊆ ℝ
o1compt.5 ⊢ φ ∧ m ∈ ℝ → ∃ x ∈ ℝ ∀ y ∈ B x ≤ y → m ≤ C
Assertion o1compt ⊢ φ → F ∘ y ∈ B ⟼ C ∈ 𝑂⁡1

Proof

Step Hyp Ref Expression
1 o1compt.1 ⊢ φ → F : A ⟶ ℂ
2 o1compt.2 ⊢ φ → F ∈ 𝑂⁡1
3 o1compt.3 ⊢ φ ∧ y ∈ B → C ∈ A
4 o1compt.4 ⊢ φ → B ⊆ ℝ
5 o1compt.5 ⊢ φ ∧ m ∈ ℝ → ∃ x ∈ ℝ ∀ y ∈ B x ≤ y → m ≤ C
6 3 fmpttd ⊢ φ → y ∈ B ⟼ C : B ⟶ A
7 nfv ⊢ Ⅎ y x ≤ z
8 nfcv ⊢ Ⅎ _ y m
9 nfcv ⊢ Ⅎ _ y ≤
10 nffvmpt1 ⊢ Ⅎ _ y y ∈ B ⟼ C ⁡ z
11 8 9 10 nfbr ⊢ Ⅎ y m ≤ y ∈ B ⟼ C ⁡ z
12 7 11 nfim ⊢ Ⅎ y x ≤ z → m ≤ y ∈ B ⟼ C ⁡ z
13 nfv ⊢ Ⅎ z x ≤ y → m ≤ y ∈ B ⟼ C ⁡ y
14 breq2 ⊢ z = y → x ≤ z ↔ x ≤ y
15 fveq2 ⊢ z = y → y ∈ B ⟼ C ⁡ z = y ∈ B ⟼ C ⁡ y
16 15 breq2d ⊢ z = y → m ≤ y ∈ B ⟼ C ⁡ z ↔ m ≤ y ∈ B ⟼ C ⁡ y
17 14 16 imbi12d ⊢ z = y → x ≤ z → m ≤ y ∈ B ⟼ C ⁡ z ↔ x ≤ y → m ≤ y ∈ B ⟼ C ⁡ y
18 12 13 17 cbvralw ⊢ ∀ z ∈ B x ≤ z → m ≤ y ∈ B ⟼ C ⁡ z ↔ ∀ y ∈ B x ≤ y → m ≤ y ∈ B ⟼ C ⁡ y
19 simpr ⊢ φ ∧ y ∈ B → y ∈ B
20 eqid ⊢ y ∈ B ⟼ C = y ∈ B ⟼ C
21 20 fvmpt2 ⊢ y ∈ B ∧ C ∈ A → y ∈ B ⟼ C ⁡ y = C
22 19 3 21 syl2anc ⊢ φ ∧ y ∈ B → y ∈ B ⟼ C ⁡ y = C
23 22 breq2d ⊢ φ ∧ y ∈ B → m ≤ y ∈ B ⟼ C ⁡ y ↔ m ≤ C
24 23 imbi2d ⊢ φ ∧ y ∈ B → x ≤ y → m ≤ y ∈ B ⟼ C ⁡ y ↔ x ≤ y → m ≤ C
25 24 ralbidva ⊢ φ → ∀ y ∈ B x ≤ y → m ≤ y ∈ B ⟼ C ⁡ y ↔ ∀ y ∈ B x ≤ y → m ≤ C
26 18 25 bitrid ⊢ φ → ∀ z ∈ B x ≤ z → m ≤ y ∈ B ⟼ C ⁡ z ↔ ∀ y ∈ B x ≤ y → m ≤ C
27 26 rexbidv ⊢ φ → ∃ x ∈ ℝ ∀ z ∈ B x ≤ z → m ≤ y ∈ B ⟼ C ⁡ z ↔ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y → m ≤ C
28 27 adantr ⊢ φ ∧ m ∈ ℝ → ∃ x ∈ ℝ ∀ z ∈ B x ≤ z → m ≤ y ∈ B ⟼ C ⁡ z ↔ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y → m ≤ C
29 5 28 mpbird ⊢ φ ∧ m ∈ ℝ → ∃ x ∈ ℝ ∀ z ∈ B x ≤ z → m ≤ y ∈ B ⟼ C ⁡ z
30 1 2 6 4 29 o1co ⊢ φ → F ∘ y ∈ B ⟼ C ∈ 𝑂⁡1