Step | Hyp | Ref
| Expression |
1 | | lo1add.3 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1)) |
2 | | lo1add.4 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1)) |
3 | | reeanv 3295 |
. . . 4
⊢
(∃𝑚 ∈
ℝ ∃𝑛 ∈
ℝ (∃𝑐 ∈
ℝ ∀𝑥 ∈
𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)) ↔ (∃𝑚 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛))) |
4 | | o1add2.1 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
5 | 4 | ralrimiva 3110 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) |
6 | | dmmptg 6143 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
8 | | lo1dm 15224 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ℝ) |
9 | 1, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ℝ) |
10 | 7, 9 | eqsstrrd 3965 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
11 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → 𝐴 ⊆ ℝ) |
12 | | rexanre 15054 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ →
(∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛)) ↔ (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)))) |
13 | 11, 12 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛)) ↔ (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)))) |
14 | | readdcl 10953 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑚 + 𝑛) ∈ ℝ) |
15 | 14 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (𝑚 + 𝑛) ∈ ℝ) |
16 | 4, 1 | lo1mptrcl 15327 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
17 | 16 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
18 | | o1add2.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) |
19 | 18, 2 | lo1mptrcl 15327 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) |
20 | 19 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) |
21 | | simplrl 774 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → 𝑚 ∈ ℝ) |
22 | | simplrr 775 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → 𝑛 ∈ ℝ) |
23 | | le2add 11455 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → ((𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛) → (𝐵 + 𝐶) ≤ (𝑚 + 𝑛))) |
24 | 17, 20, 21, 22, 23 | syl22anc 836 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛) → (𝐵 + 𝐶) ≤ (𝑚 + 𝑛))) |
25 | 24 | imim2d 57 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) ∧ 𝑥 ∈ 𝐴) → ((𝑐 ≤ 𝑥 → (𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛)) → (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ (𝑚 + 𝑛)))) |
26 | 25 | ralimdva 3105 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛)) → ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ (𝑚 + 𝑛)))) |
27 | | breq2 5083 |
. . . . . . . . . . 11
⊢ (𝑝 = (𝑚 + 𝑛) → ((𝐵 + 𝐶) ≤ 𝑝 ↔ (𝐵 + 𝐶) ≤ (𝑚 + 𝑛))) |
28 | 27 | imbi2d 341 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑚 + 𝑛) → ((𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ 𝑝) ↔ (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ (𝑚 + 𝑛)))) |
29 | 28 | ralbidv 3123 |
. . . . . . . . 9
⊢ (𝑝 = (𝑚 + 𝑛) → (∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ 𝑝) ↔ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ (𝑚 + 𝑛)))) |
30 | 29 | rspcev 3561 |
. . . . . . . 8
⊢ (((𝑚 + 𝑛) ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ (𝑚 + 𝑛))) → ∃𝑝 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ 𝑝)) |
31 | 15, 26, 30 | syl6an 681 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛)) → ∃𝑝 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ 𝑝))) |
32 | 31 | reximdv 3204 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 ≤ 𝑚 ∧ 𝐶 ≤ 𝑛)) → ∃𝑐 ∈ ℝ ∃𝑝 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ 𝑝))) |
33 | 13, 32 | sylbird 259 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑛 ∈ ℝ)) → ((∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)) → ∃𝑐 ∈ ℝ ∃𝑝 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ 𝑝))) |
34 | 33 | rexlimdvva 3225 |
. . . 4
⊢ (𝜑 → (∃𝑚 ∈ ℝ ∃𝑛 ∈ ℝ (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)) → ∃𝑐 ∈ ℝ ∃𝑝 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ 𝑝))) |
35 | 3, 34 | syl5bir 242 |
. . 3
⊢ (𝜑 → ((∃𝑚 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)) → ∃𝑐 ∈ ℝ ∃𝑝 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ 𝑝))) |
36 | 10, 16 | ello1mpt 15226 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔
∃𝑐 ∈ ℝ
∃𝑚 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚))) |
37 | | rexcom 3284 |
. . . . 5
⊢
(∃𝑐 ∈
ℝ ∃𝑚 ∈
ℝ ∀𝑥 ∈
𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ↔ ∃𝑚 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚)) |
38 | 36, 37 | bitrdi 287 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ↔
∃𝑚 ∈ ℝ
∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚))) |
39 | 10, 19 | ello1mpt 15226 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1) ↔
∃𝑐 ∈ ℝ
∃𝑛 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛))) |
40 | | rexcom 3284 |
. . . . 5
⊢
(∃𝑐 ∈
ℝ ∃𝑛 ∈
ℝ ∀𝑥 ∈
𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛) ↔ ∃𝑛 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)) |
41 | 39, 40 | bitrdi 287 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1) ↔
∃𝑛 ∈ ℝ
∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛))) |
42 | 38, 41 | anbi12d 631 |
. . 3
⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1)) ↔
(∃𝑚 ∈ ℝ
∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐵 ≤ 𝑚) ∧ ∃𝑛 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → 𝐶 ≤ 𝑛)))) |
43 | 16, 19 | readdcld 11003 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℝ) |
44 | 10, 43 | ello1mpt 15226 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ ≤𝑂(1) ↔
∃𝑐 ∈ ℝ
∃𝑝 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (𝐵 + 𝐶) ≤ 𝑝))) |
45 | 35, 42, 44 | 3imtr4d 294 |
. 2
⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ ≤𝑂(1) ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ ≤𝑂(1)) → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈
≤𝑂(1))) |
46 | 1, 2, 45 | mp2and 696 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ ≤𝑂(1)) |