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 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
o1add2.2 ( ( 𝜑𝑥𝐴 ) → 𝐶𝑉 )
o1add2.3 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) )
o1add2.4 ( 𝜑 → ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) )
Assertion o1sub2 ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 o1add2.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
2 o1add2.2 ( ( 𝜑𝑥𝐴 ) → 𝐶𝑉 )
3 o1add2.3 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) )
4 o1add2.4 ( 𝜑 → ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) )
5 1 ralrimiva ( 𝜑 → ∀ 𝑥𝐴 𝐵𝑉 )
6 dmmptg ( ∀ 𝑥𝐴 𝐵𝑉 → dom ( 𝑥𝐴𝐵 ) = 𝐴 )
7 5 6 syl ( 𝜑 → dom ( 𝑥𝐴𝐵 ) = 𝐴 )
8 o1dm ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) → dom ( 𝑥𝐴𝐵 ) ⊆ ℝ )
9 3 8 syl ( 𝜑 → dom ( 𝑥𝐴𝐵 ) ⊆ ℝ )
10 7 9 eqsstrrd ( 𝜑𝐴 ⊆ ℝ )
11 reex ℝ ∈ V
12 11 ssex ( 𝐴 ⊆ ℝ → 𝐴 ∈ V )
13 10 12 syl ( 𝜑𝐴 ∈ V )
14 eqidd ( 𝜑 → ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 ) )
15 eqidd ( 𝜑 → ( 𝑥𝐴𝐶 ) = ( 𝑥𝐴𝐶 ) )
16 13 1 2 14 15 offval2 ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∘f − ( 𝑥𝐴𝐶 ) ) = ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) )
17 o1sub ( ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ∧ ( 𝑥𝐴𝐶 ) ∈ 𝑂(1) ) → ( ( 𝑥𝐴𝐵 ) ∘f − ( 𝑥𝐴𝐶 ) ) ∈ 𝑂(1) )
18 3 4 17 syl2anc ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∘f − ( 𝑥𝐴𝐶 ) ) ∈ 𝑂(1) )
19 16 18 eqeltrrd ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐵𝐶 ) ) ∈ 𝑂(1) )