Metamath Proof Explorer


Theorem o1add2

Description: The sum 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 o1add2 φ 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 o1add 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