Metamath Proof Explorer

Theorem o1mul2

Description: The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1add2.1 ⊢ φ ∧ x ∈ A → B ∈ V
o1add2.2 ⊢ φ ∧ x ∈ A → C ∈ V
o1add2.3 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1
o1add2.4 ⊢ φ → x ∈ A ⟼ C ∈ 𝑂⁡1
Assertion o1mul2 ⊢ φ → x ∈ A ⟼ B ⁢ C ∈ 𝑂⁡1

Proof

Step Hyp Ref Expression
1 o1add2.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 o1add2.2 ⊢ φ ∧ x ∈ A → C ∈ V
3 o1add2.3 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1
4 o1add2.4 ⊢ φ → x ∈ A ⟼ C ∈ 𝑂⁡1
5 1 ralrimiva ⊢ φ → ∀ x ∈ A B ∈ V
6 dmmptg ⊢ ∀ x ∈ A B ∈ V → dom ⁡ x ∈ A ⟼ B = A
7 5 6 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B = A
8 o1dm ⊢ x ∈ A ⟼ B ∈ 𝑂⁡1 → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
9 3 8 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
10 7 9 eqsstrrd ⊢ φ → A ⊆ ℝ
11 reex ⊢ ℝ ∈ V
12 11 ssex ⊢ A ⊆ ℝ → A ∈ V
13 10 12 syl ⊢ φ → A ∈ V
14 eqidd ⊢ φ → x ∈ A ⟼ B = x ∈ A ⟼ B
15 eqidd ⊢ φ → x ∈ A ⟼ C = x ∈ A ⟼ C
16 13 1 2 14 15 offval2 ⊢ φ → x ∈ A ⟼ B × f x ∈ A ⟼ C = x ∈ A ⟼ B ⁢ C
17 o1mul ⊢ x ∈ A ⟼ B ∈ 𝑂⁡1 ∧ x ∈ A ⟼ C ∈ 𝑂⁡1 → x ∈ A ⟼ B × f x ∈ A ⟼ C ∈ 𝑂⁡1
18 3 4 17 syl2anc ⊢ φ → x ∈ A ⟼ B × f x ∈ A ⟼ C ∈ 𝑂⁡1
19 16 18 eqeltrrd ⊢ φ → x ∈ A ⟼ B ⁢ C ∈ 𝑂⁡1