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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	o1add2.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
	o1add2.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )
	o1add2.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) )
Assertion	o1mul2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ∈ 𝑂(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		o1mul	⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∘f · ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) ∈ 𝑂(1) )
18	3 4 17	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∘f · ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) ∈ 𝑂(1) )
19	16 18	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) ) ∈ 𝑂(1) )