Step | Hyp | Ref
| Expression |
1 | | readdcl 9898 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ) |
2 | 1 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ) |
3 | | mbfadd.3 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
4 | | mbfadd.4 |
. . 3
⊢ (𝜑 → 𝐺:𝐴⟶ℝ) |
5 | | fdm 5964 |
. . . . 5
⊢ (𝐹:𝐴⟶ℝ → dom 𝐹 = 𝐴) |
6 | 3, 5 | syl 17 |
. . . 4
⊢ (𝜑 → dom 𝐹 = 𝐴) |
7 | | mbfadd.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ MblFn) |
8 | | mbfdm 23201 |
. . . . 5
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝜑 → dom 𝐹 ∈ dom vol) |
10 | 6, 9 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → 𝐴 ∈ dom vol) |
11 | | inidm 3784 |
. . 3
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
12 | 2, 3, 4, 10, 10, 11 | off 6810 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):𝐴⟶ℝ) |
13 | | eliun 4460 |
. . . . 5
⊢ (𝑥 ∈ ∪ 𝑟 ∈ ℚ ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ↔ ∃𝑟 ∈ ℚ 𝑥 ∈ ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞)))) |
14 | | r19.42v 3073 |
. . . . . . 7
⊢
(∃𝑟 ∈
ℚ (𝑥 ∈ 𝐴 ∧ ((𝐹‘𝑥) ∈ (𝑟(,)+∞) ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞))) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑟 ∈ ℚ ((𝐹‘𝑥) ∈ (𝑟(,)+∞) ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞)))) |
15 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ) |
16 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐺:𝐴⟶ℝ) |
17 | 16 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℝ) |
18 | 3 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐹:𝐴⟶ℝ) |
19 | 18 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) |
20 | 15, 17, 19 | ltsubaddd 10502 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝑦 − (𝐺‘𝑥)) < (𝐹‘𝑥) ↔ 𝑦 < ((𝐹‘𝑥) + (𝐺‘𝑥)))) |
21 | 15 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → 𝑦 ∈ ℝ) |
22 | | qre 11669 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 ∈ ℚ → 𝑟 ∈
ℝ) |
23 | 22 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → 𝑟 ∈ ℝ) |
24 | 17 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → (𝐺‘𝑥) ∈ ℝ) |
25 | | ltsub23 10387 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ ∧ (𝐺‘𝑥) ∈ ℝ) → ((𝑦 − 𝑟) < (𝐺‘𝑥) ↔ (𝑦 − (𝐺‘𝑥)) < 𝑟)) |
26 | 21, 23, 24, 25 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → ((𝑦 − 𝑟) < (𝐺‘𝑥) ↔ (𝑦 − (𝐺‘𝑥)) < 𝑟)) |
27 | 26 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → ((𝑟 < (𝐹‘𝑥) ∧ (𝑦 − 𝑟) < (𝐺‘𝑥)) ↔ (𝑟 < (𝐹‘𝑥) ∧ (𝑦 − (𝐺‘𝑥)) < 𝑟))) |
28 | | ancom 465 |
. . . . . . . . . . . . 13
⊢ ((𝑟 < (𝐹‘𝑥) ∧ (𝑦 − (𝐺‘𝑥)) < 𝑟) ↔ ((𝑦 − (𝐺‘𝑥)) < 𝑟 ∧ 𝑟 < (𝐹‘𝑥))) |
29 | 27, 28 | syl6bb 275 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → ((𝑟 < (𝐹‘𝑥) ∧ (𝑦 − 𝑟) < (𝐺‘𝑥)) ↔ ((𝑦 − (𝐺‘𝑥)) < 𝑟 ∧ 𝑟 < (𝐹‘𝑥)))) |
30 | 29 | rexbidva 3031 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑟 ∈ ℚ (𝑟 < (𝐹‘𝑥) ∧ (𝑦 − 𝑟) < (𝐺‘𝑥)) ↔ ∃𝑟 ∈ ℚ ((𝑦 − (𝐺‘𝑥)) < 𝑟 ∧ 𝑟 < (𝐹‘𝑥)))) |
31 | 15, 17 | resubcld 10337 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑦 − (𝐺‘𝑥)) ∈ ℝ) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → (𝑦 − (𝐺‘𝑥)) ∈ ℝ) |
33 | 19 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → (𝐹‘𝑥) ∈ ℝ) |
34 | | lttr 9993 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 − (𝐺‘𝑥)) ∈ ℝ ∧ 𝑟 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → (((𝑦 − (𝐺‘𝑥)) < 𝑟 ∧ 𝑟 < (𝐹‘𝑥)) → (𝑦 − (𝐺‘𝑥)) < (𝐹‘𝑥))) |
35 | 32, 23, 33, 34 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → (((𝑦 − (𝐺‘𝑥)) < 𝑟 ∧ 𝑟 < (𝐹‘𝑥)) → (𝑦 − (𝐺‘𝑥)) < (𝐹‘𝑥))) |
36 | 35 | rexlimdva 3013 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑟 ∈ ℚ ((𝑦 − (𝐺‘𝑥)) < 𝑟 ∧ 𝑟 < (𝐹‘𝑥)) → (𝑦 − (𝐺‘𝑥)) < (𝐹‘𝑥))) |
37 | | qbtwnre 11904 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 − (𝐺‘𝑥)) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ (𝑦 − (𝐺‘𝑥)) < (𝐹‘𝑥)) → ∃𝑟 ∈ ℚ ((𝑦 − (𝐺‘𝑥)) < 𝑟 ∧ 𝑟 < (𝐹‘𝑥))) |
38 | 37 | 3expia 1259 |
. . . . . . . . . . . . 13
⊢ (((𝑦 − (𝐺‘𝑥)) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → ((𝑦 − (𝐺‘𝑥)) < (𝐹‘𝑥) → ∃𝑟 ∈ ℚ ((𝑦 − (𝐺‘𝑥)) < 𝑟 ∧ 𝑟 < (𝐹‘𝑥)))) |
39 | 31, 19, 38 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝑦 − (𝐺‘𝑥)) < (𝐹‘𝑥) → ∃𝑟 ∈ ℚ ((𝑦 − (𝐺‘𝑥)) < 𝑟 ∧ 𝑟 < (𝐹‘𝑥)))) |
40 | 36, 39 | impbid 201 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑟 ∈ ℚ ((𝑦 − (𝐺‘𝑥)) < 𝑟 ∧ 𝑟 < (𝐹‘𝑥)) ↔ (𝑦 − (𝐺‘𝑥)) < (𝐹‘𝑥))) |
41 | 30, 40 | bitrd 267 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑟 ∈ ℚ (𝑟 < (𝐹‘𝑥) ∧ (𝑦 − 𝑟) < (𝐺‘𝑥)) ↔ (𝑦 − (𝐺‘𝑥)) < (𝐹‘𝑥))) |
42 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐴⟶ℝ → 𝐹 Fn 𝐴) |
43 | 3, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn 𝐴) |
44 | 43 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐹 Fn 𝐴) |
45 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝐺:𝐴⟶ℝ → 𝐺 Fn 𝐴) |
46 | 4, 45 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 Fn 𝐴) |
47 | 46 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐺 Fn 𝐴) |
48 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐴 ∈ dom vol) |
49 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
50 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
51 | 44, 47, 48, 48, 11, 49, 50 | ofval 6804 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘𝑓 + 𝐺)‘𝑥) = ((𝐹‘𝑥) + (𝐺‘𝑥))) |
52 | 51 | breq2d 4595 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑦 < ((𝐹 ∘𝑓 + 𝐺)‘𝑥) ↔ 𝑦 < ((𝐹‘𝑥) + (𝐺‘𝑥)))) |
53 | 20, 41, 52 | 3bitr4d 299 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑟 ∈ ℚ (𝑟 < (𝐹‘𝑥) ∧ (𝑦 − 𝑟) < (𝐺‘𝑥)) ↔ 𝑦 < ((𝐹 ∘𝑓 + 𝐺)‘𝑥))) |
54 | 23 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → 𝑟 ∈ ℝ*) |
55 | | elioopnf 12138 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ*
→ ((𝐹‘𝑥) ∈ (𝑟(,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑟 < (𝐹‘𝑥)))) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → ((𝐹‘𝑥) ∈ (𝑟(,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑟 < (𝐹‘𝑥)))) |
57 | 33 | biantrurd 528 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → (𝑟 < (𝐹‘𝑥) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑟 < (𝐹‘𝑥)))) |
58 | 56, 57 | bitr4d 270 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → ((𝐹‘𝑥) ∈ (𝑟(,)+∞) ↔ 𝑟 < (𝐹‘𝑥))) |
59 | 21, 23 | resubcld 10337 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → (𝑦 − 𝑟) ∈ ℝ) |
60 | 59 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → (𝑦 − 𝑟) ∈
ℝ*) |
61 | | elioopnf 12138 |
. . . . . . . . . . . . 13
⊢ ((𝑦 − 𝑟) ∈ ℝ* → ((𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞) ↔ ((𝐺‘𝑥) ∈ ℝ ∧ (𝑦 − 𝑟) < (𝐺‘𝑥)))) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → ((𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞) ↔ ((𝐺‘𝑥) ∈ ℝ ∧ (𝑦 − 𝑟) < (𝐺‘𝑥)))) |
63 | 24 | biantrurd 528 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → ((𝑦 − 𝑟) < (𝐺‘𝑥) ↔ ((𝐺‘𝑥) ∈ ℝ ∧ (𝑦 − 𝑟) < (𝐺‘𝑥)))) |
64 | 62, 63 | bitr4d 270 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → ((𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞) ↔ (𝑦 − 𝑟) < (𝐺‘𝑥))) |
65 | 58, 64 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ 𝑟 ∈ ℚ) → (((𝐹‘𝑥) ∈ (𝑟(,)+∞) ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞)) ↔ (𝑟 < (𝐹‘𝑥) ∧ (𝑦 − 𝑟) < (𝐺‘𝑥)))) |
66 | 65 | rexbidva 3031 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑟 ∈ ℚ ((𝐹‘𝑥) ∈ (𝑟(,)+∞) ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞)) ↔ ∃𝑟 ∈ ℚ (𝑟 < (𝐹‘𝑥) ∧ (𝑦 − 𝑟) < (𝐺‘𝑥)))) |
67 | 15 | rexrd 9968 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
68 | | elioopnf 12138 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
→ (((𝐹
∘𝑓 + 𝐺)‘𝑥) ∈ (𝑦(,)+∞) ↔ (((𝐹 ∘𝑓 + 𝐺)‘𝑥) ∈ ℝ ∧ 𝑦 < ((𝐹 ∘𝑓 + 𝐺)‘𝑥)))) |
69 | 67, 68 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (((𝐹 ∘𝑓 + 𝐺)‘𝑥) ∈ (𝑦(,)+∞) ↔ (((𝐹 ∘𝑓 + 𝐺)‘𝑥) ∈ ℝ ∧ 𝑦 < ((𝐹 ∘𝑓 + 𝐺)‘𝑥)))) |
70 | 12 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹 ∘𝑓 + 𝐺):𝐴⟶ℝ) |
71 | 70 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘𝑓 + 𝐺)‘𝑥) ∈ ℝ) |
72 | 71 | biantrurd 528 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑦 < ((𝐹 ∘𝑓 + 𝐺)‘𝑥) ↔ (((𝐹 ∘𝑓 + 𝐺)‘𝑥) ∈ ℝ ∧ 𝑦 < ((𝐹 ∘𝑓 + 𝐺)‘𝑥)))) |
73 | 69, 72 | bitr4d 270 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (((𝐹 ∘𝑓 + 𝐺)‘𝑥) ∈ (𝑦(,)+∞) ↔ 𝑦 < ((𝐹 ∘𝑓 + 𝐺)‘𝑥))) |
74 | 53, 66, 73 | 3bitr4d 299 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (∃𝑟 ∈ ℚ ((𝐹‘𝑥) ∈ (𝑟(,)+∞) ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞)) ↔ ((𝐹 ∘𝑓 + 𝐺)‘𝑥) ∈ (𝑦(,)+∞))) |
75 | 74 | pm5.32da 671 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ 𝐴 ∧ ∃𝑟 ∈ ℚ ((𝐹‘𝑥) ∈ (𝑟(,)+∞) ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞))) ↔ (𝑥 ∈ 𝐴 ∧ ((𝐹 ∘𝑓 + 𝐺)‘𝑥) ∈ (𝑦(,)+∞)))) |
76 | 14, 75 | syl5bb 271 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑟 ∈ ℚ (𝑥 ∈ 𝐴 ∧ ((𝐹‘𝑥) ∈ (𝑟(,)+∞) ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞))) ↔ (𝑥 ∈ 𝐴 ∧ ((𝐹 ∘𝑓 + 𝐺)‘𝑥) ∈ (𝑦(,)+∞)))) |
77 | | elpreima 6245 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ (◡𝐹 “ (𝑟(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (𝑟(,)+∞)))) |
78 | 44, 77 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (𝑟(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (𝑟(,)+∞)))) |
79 | | elpreima 6245 |
. . . . . . . . . 10
⊢ (𝐺 Fn 𝐴 → (𝑥 ∈ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞)))) |
80 | 47, 79 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑥 ∈ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞)))) |
81 | 78, 80 | anbi12d 743 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((𝑥 ∈ (◡𝐹 “ (𝑟(,)+∞)) ∧ 𝑥 ∈ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ↔ ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (𝑟(,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞))))) |
82 | | elin 3758 |
. . . . . . . 8
⊢ (𝑥 ∈ ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ↔ (𝑥 ∈ (◡𝐹 “ (𝑟(,)+∞)) ∧ 𝑥 ∈ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞)))) |
83 | | anandi 867 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝐹‘𝑥) ∈ (𝑟(,)+∞) ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞))) ↔ ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ∈ (𝑟(,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞)))) |
84 | 81, 82, 83 | 3bitr4g 302 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑥 ∈ ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ↔ (𝑥 ∈ 𝐴 ∧ ((𝐹‘𝑥) ∈ (𝑟(,)+∞) ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞))))) |
85 | 84 | rexbidv 3034 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑟 ∈ ℚ 𝑥 ∈ ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ↔ ∃𝑟 ∈ ℚ (𝑥 ∈ 𝐴 ∧ ((𝐹‘𝑥) ∈ (𝑟(,)+∞) ∧ (𝐺‘𝑥) ∈ ((𝑦 − 𝑟)(,)+∞))))) |
86 | | ffn 5958 |
. . . . . . . . 9
⊢ ((𝐹 ∘𝑓 +
𝐺):𝐴⟶ℝ → (𝐹 ∘𝑓 + 𝐺) Fn 𝐴) |
87 | 12, 86 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) Fn 𝐴) |
88 | 87 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹 ∘𝑓 + 𝐺) Fn 𝐴) |
89 | | elpreima 6245 |
. . . . . . 7
⊢ ((𝐹 ∘𝑓 +
𝐺) Fn 𝐴 → (𝑥 ∈ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝐹 ∘𝑓 + 𝐺)‘𝑥) ∈ (𝑦(,)+∞)))) |
90 | 88, 89 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑥 ∈ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑦(,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ ((𝐹 ∘𝑓 + 𝐺)‘𝑥) ∈ (𝑦(,)+∞)))) |
91 | 76, 85, 90 | 3bitr4d 299 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑟 ∈ ℚ 𝑥 ∈ ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ↔ 𝑥 ∈ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑦(,)+∞)))) |
92 | 13, 91 | syl5bb 271 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑥 ∈ ∪
𝑟 ∈ ℚ ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ↔ 𝑥 ∈ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑦(,)+∞)))) |
93 | 92 | eqrdv 2608 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∪ 𝑟 ∈ ℚ ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) = (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑦(,)+∞))) |
94 | | qnnen 14781 |
. . . . 5
⊢ ℚ
≈ ℕ |
95 | | endom 7868 |
. . . . 5
⊢ (ℚ
≈ ℕ → ℚ ≼ ℕ) |
96 | 94, 95 | ax-mp 5 |
. . . 4
⊢ ℚ
≼ ℕ |
97 | | mbfima 23205 |
. . . . . . . 8
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ (𝑟(,)+∞)) ∈ dom
vol) |
98 | 7, 3, 97 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (◡𝐹 “ (𝑟(,)+∞)) ∈ dom
vol) |
99 | | mbfadd.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ MblFn) |
100 | | mbfima 23205 |
. . . . . . . 8
⊢ ((𝐺 ∈ MblFn ∧ 𝐺:𝐴⟶ℝ) → (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞)) ∈ dom
vol) |
101 | 99, 4, 100 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞)) ∈ dom
vol) |
102 | | inmbl 23117 |
. . . . . . 7
⊢ (((◡𝐹 “ (𝑟(,)+∞)) ∈ dom vol ∧ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞)) ∈ dom vol) → ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ∈ dom
vol) |
103 | 98, 101, 102 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ∈ dom
vol) |
104 | 103 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℚ) → ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ∈ dom
vol) |
105 | 104 | ralrimiva 2949 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∀𝑟 ∈ ℚ ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ∈ dom
vol) |
106 | | iunmbl2 23132 |
. . . 4
⊢ ((ℚ
≼ ℕ ∧ ∀𝑟 ∈ ℚ ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ∈ dom vol) →
∪ 𝑟 ∈ ℚ ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ∈ dom
vol) |
107 | 96, 105, 106 | sylancr 694 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∪ 𝑟 ∈ ℚ ((◡𝐹 “ (𝑟(,)+∞)) ∩ (◡𝐺 “ ((𝑦 − 𝑟)(,)+∞))) ∈ dom
vol) |
108 | 93, 107 | eqeltrrd 2689 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑦(,)+∞)) ∈ dom
vol) |
109 | 12, 108 | ismbf3d 23227 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ MblFn) |