Metamath Proof Explorer

Theorem o1sub2

Description: The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014)

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 o1sub2 ⊢ φ → 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 o1sub ⊢ 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