Metamath Proof Explorer

Theorem lo1add

Description: The sum of two eventually upper bounded functions is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1add2.1 ⊢ φ ∧ x ∈ A → B ∈ V
o1add2.2 ⊢ φ ∧ x ∈ A → C ∈ V
lo1add.3 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
lo1add.4 ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1
Assertion lo1add ⊢ φ → 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 lo1add.3 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1
4 lo1add.4 ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1
5 reeanv ⊢ ∃ m ∈ ℝ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n ↔ ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
6 1 ralrimiva ⊢ φ → ∀ x ∈ A B ∈ V
7 dmmptg ⊢ ∀ x ∈ A B ∈ V → dom ⁡ x ∈ A ⟼ B = A
8 6 7 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B = A
9 lo1dm ⊢ x ∈ A ⟼ B ∈ ≤𝑂⁡1 → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
10 3 9 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B ⊆ ℝ
11 8 10 eqsstrrd ⊢ φ → A ⊆ ℝ
12 11 adantr ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → A ⊆ ℝ
13 rexanre ⊢ A ⊆ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ C ≤ n ↔ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
14 12 13 syl ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ C ≤ n ↔ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
15 readdcl ⊢ m ∈ ℝ ∧ n ∈ ℝ → m + n ∈ ℝ
16 15 adantl ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → m + n ∈ ℝ
17 1 3 lo1mptrcl ⊢ φ ∧ x ∈ A → B ∈ ℝ
18 17 adantlr ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → B ∈ ℝ
19 2 4 lo1mptrcl ⊢ φ ∧ x ∈ A → C ∈ ℝ
20 19 adantlr ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → C ∈ ℝ
21 simplrl ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → m ∈ ℝ
22 simplrr ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → n ∈ ℝ
23 le2add ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ m ∈ ℝ ∧ n ∈ ℝ → B ≤ m ∧ C ≤ n → B + C ≤ m + n
24 18 20 21 22 23 syl22anc ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → B ≤ m ∧ C ≤ n → B + C ≤ m + n
25 24 imim2d ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ ∧ x ∈ A → c ≤ x → B ≤ m ∧ C ≤ n → c ≤ x → B + C ≤ m + n
26 25 ralimdva ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → ∀ x ∈ A c ≤ x → B ≤ m ∧ C ≤ n → ∀ x ∈ A c ≤ x → B + C ≤ m + n
27 breq2 ⊢ p = m + n → B + C ≤ p ↔ B + C ≤ m + n
28 27 imbi2d ⊢ p = m + n → c ≤ x → B + C ≤ p ↔ c ≤ x → B + C ≤ m + n
29 28 ralbidv ⊢ p = m + n → ∀ x ∈ A c ≤ x → B + C ≤ p ↔ ∀ x ∈ A c ≤ x → B + C ≤ m + n
30 29 rspcev ⊢ m + n ∈ ℝ ∧ ∀ x ∈ A c ≤ x → B + C ≤ m + n → ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B + C ≤ p
31 16 26 30 syl6an ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → ∀ x ∈ A c ≤ x → B ≤ m ∧ C ≤ n → ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B + C ≤ p
32 31 reximdv ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ C ≤ n → ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B + C ≤ p
33 14 32 sylbird ⊢ φ ∧ m ∈ ℝ ∧ n ∈ ℝ → ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n → ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B + C ≤ p
34 33 rexlimdvva ⊢ φ → ∃ m ∈ ℝ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n → ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B + C ≤ p
35 5 34 syl5bir ⊢ φ → ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n → ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B + C ≤ p
36 11 17 ello1mpt ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ c ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m
37 rexcom ⊢ ∃ c ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ↔ ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m
38 36 37 bitrdi ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m
39 11 19 ello1mpt ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1 ↔ ∃ c ∈ ℝ ∃ n ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
40 rexcom ⊢ ∃ c ∈ ℝ ∃ n ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n ↔ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
41 39 40 bitrdi ⊢ φ → x ∈ A ⟼ C ∈ ≤𝑂⁡1 ↔ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
42 38 41 anbi12d ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ C ∈ ≤𝑂⁡1 ↔ ∃ m ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → B ≤ m ∧ ∃ n ∈ ℝ ∃ c ∈ ℝ ∀ x ∈ A c ≤ x → C ≤ n
43 17 19 readdcld ⊢ φ ∧ x ∈ A → B + C ∈ ℝ
44 11 43 ello1mpt ⊢ φ → x ∈ A ⟼ B + C ∈ ≤𝑂⁡1 ↔ ∃ c ∈ ℝ ∃ p ∈ ℝ ∀ x ∈ A c ≤ x → B + C ≤ p
45 35 42 44 3imtr4d ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ∧ x ∈ A ⟼ C ∈ ≤𝑂⁡1 → x ∈ A ⟼ B + C ∈ ≤𝑂⁡1
46 3 4 45 mp2and ⊢ φ → x ∈ A ⟼ B + C ∈ ≤𝑂⁡1