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	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	o1add2.2	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
	o1add2.3	$$⊢\phi \to \left(x\in A⟼B\right)\in 𝑂\left(1\right)$$
	o1add2.4	$$⊢\phi \to \left(x\in A⟼C\right)\in 𝑂\left(1\right)$$
Assertion	o1mul2	$$⊢\phi \to \left(x\in A⟼BC\right)\in 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		o1add2.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
2		o1add2.2	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
3		o1add2.3	$$⊢\phi \to \left(x\in A⟼B\right)\in 𝑂\left(1\right)$$
4		o1add2.4	$$⊢\phi \to \left(x\in A⟼C\right)\in 𝑂\left(1\right)$$
5	1	ralrimiva	$$⊢\phi \to \forall x\in AB\in V$$
6		dmmptg	$$⊢\forall x\in AB\in V\to \mathrm{dom}\left(x\in A⟼B\right)=A$$
7	5 6	syl	$$⊢\phi \to \mathrm{dom}\left(x\in A⟼B\right)=A$$
8		o1dm	$$⊢\left(x\in A⟼B\right)\in 𝑂\left(1\right)\to \mathrm{dom}\left(x\in A⟼B\right)\subseteq ℝ$$
9	3 8	syl	$$⊢\phi \to \mathrm{dom}\left(x\in A⟼B\right)\subseteq ℝ$$
10	7 9	eqsstrrd	$$⊢\phi \to A\subseteq ℝ$$
11		reex	$$⊢ℝ\in \mathrm{V}$$
12	11	ssex	$$⊢A\subseteq ℝ\to A\in \mathrm{V}$$
13	10 12	syl	$$⊢\phi \to A\in \mathrm{V}$$
14		eqidd	$$⊢\phi \to \left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
15		eqidd	$$⊢\phi \to \left(x\in A⟼C\right)=\left(x\in A⟼C\right)$$
16	13 1 2 14 15	offval2	$$⊢\phi \to \left(x\in A⟼B\right){\times }_f\left(x\in A⟼C\right)=\left(x\in A⟼BC\right)$$
17		o1mul	$$⊢\left(\left(x\in A⟼B\right)\in 𝑂\left(1\right)\wedge \left(x\in A⟼C\right)\in 𝑂\left(1\right)\right)\to \left(x\in A⟼B\right){\times }_f\left(x\in A⟼C\right)\in 𝑂\left(1\right)$$
18	3 4 17	syl2anc	$$⊢\phi \to \left(x\in A⟼B\right){\times }_f\left(x\in A⟼C\right)\in 𝑂\left(1\right)$$
19	16 18	eqeltrrd	$$⊢\phi \to \left(x\in A⟼BC\right)\in 𝑂\left(1\right)$$