Metamath Proof Explorer

Theorem mbfaddlem

Description: The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014)

Ref Expression
Hypotheses mbfadd.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
mbfadd.2 ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
mbfadd.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
mbfadd.4 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℝ )
Assertion mbfaddlem ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfadd.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2 mbfadd.2 ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
3 mbfadd.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
4 mbfadd.4 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℝ )
5 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
6 5 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
7 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
8 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
9 1 8 syl ⊢ ( 𝜑 → dom 𝐹 ∈ dom vol )
10 7 9 eqeltrrd ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
11 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
12 6 3 4 10 10 11 off ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) : 𝐴 ⟶ ℝ )
13 eliun ⊢ ( 𝑥 ∈ ∪ 𝑟 ∈ ℚ ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ↔ ∃ 𝑟 ∈ ℚ 𝑥 ∈ ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) )
14 r19.42v ⊢ ( ∃ 𝑟 ∈ ℚ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑟 ∈ ℚ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) )
15 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
16 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐺 : 𝐴 ⟶ ℝ )
17 16 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
18 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐹 : 𝐴 ⟶ ℝ )
19 18 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
20 15 17 19 ltsubaddd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 < ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) )
21 15 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → 𝑦 ∈ ℝ )
22 qre ⊢ ( 𝑟 ∈ ℚ → 𝑟 ∈ ℝ )
23 22 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → 𝑟 ∈ ℝ )
24 17 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
25 ltsub23 ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝑦 − 𝑟 ) < ( 𝐺 ‘ 𝑥 ) ↔ ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < 𝑟 ) )
26 21 23 24 25 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( ( 𝑦 − 𝑟 ) < ( 𝐺 ‘ 𝑥 ) ↔ ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < 𝑟 ) )
27 26 anbi1cd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( ( 𝑟 < ( 𝐹 ‘ 𝑥 ) ∧ ( 𝑦 − 𝑟 ) < ( 𝐺 ‘ 𝑥 ) ) ↔ ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < 𝑟 ∧ 𝑟 < ( 𝐹 ‘ 𝑥 ) ) ) )
28 27 rexbidva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ ℚ ( 𝑟 < ( 𝐹 ‘ 𝑥 ) ∧ ( 𝑦 − 𝑟 ) < ( 𝐺 ‘ 𝑥 ) ) ↔ ∃ 𝑟 ∈ ℚ ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < 𝑟 ∧ 𝑟 < ( 𝐹 ‘ 𝑥 ) ) ) )
29 15 17 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
30 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
31 19 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
32 lttr ⊢ ( ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ ∧ 𝑟 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) → ( ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < 𝑟 ∧ 𝑟 < ( 𝐹 ‘ 𝑥 ) ) → ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < ( 𝐹 ‘ 𝑥 ) ) )
33 30 23 31 32 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < 𝑟 ∧ 𝑟 < ( 𝐹 ‘ 𝑥 ) ) → ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < ( 𝐹 ‘ 𝑥 ) ) )
34 33 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ ℚ ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < 𝑟 ∧ 𝑟 < ( 𝐹 ‘ 𝑥 ) ) → ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < ( 𝐹 ‘ 𝑥 ) ) )
35 qbtwnre ⊢ ( ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑟 ∈ ℚ ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < 𝑟 ∧ 𝑟 < ( 𝐹 ‘ 𝑥 ) ) )
36 35 3expia ⊢ ( ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) → ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < ( 𝐹 ‘ 𝑥 ) → ∃ 𝑟 ∈ ℚ ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < 𝑟 ∧ 𝑟 < ( 𝐹 ‘ 𝑥 ) ) ) )
37 29 19 36 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < ( 𝐹 ‘ 𝑥 ) → ∃ 𝑟 ∈ ℚ ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < 𝑟 ∧ 𝑟 < ( 𝐹 ‘ 𝑥 ) ) ) )
38 34 37 impbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ ℚ ( ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < 𝑟 ∧ 𝑟 < ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < ( 𝐹 ‘ 𝑥 ) ) )
39 28 38 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ ℚ ( 𝑟 < ( 𝐹 ‘ 𝑥 ) ∧ ( 𝑦 − 𝑟 ) < ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝑦 − ( 𝐺 ‘ 𝑥 ) ) < ( 𝐹 ‘ 𝑥 ) ) )
40 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐹 Fn 𝐴 )
42 4 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐺 Fn 𝐴 )
44 10 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐴 ∈ dom vol )
45 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
46 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
47 41 43 44 44 11 45 46 ofval ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
48 47 breq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ↔ 𝑦 < ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) )
49 20 39 48 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ ℚ ( 𝑟 < ( 𝐹 ‘ 𝑥 ) ∧ ( 𝑦 − 𝑟 ) < ( 𝐺 ‘ 𝑥 ) ) ↔ 𝑦 < ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ) )
50 23 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → 𝑟 ∈ ℝ* )
51 elioopnf ⊢ ( 𝑟 ∈ ℝ* → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑟 < ( 𝐹 ‘ 𝑥 ) ) ) )
52 50 51 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑟 < ( 𝐹 ‘ 𝑥 ) ) ) )
53 31 52 mpbirand ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ↔ 𝑟 < ( 𝐹 ‘ 𝑥 ) ) )
54 21 23 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( 𝑦 − 𝑟 ) ∈ ℝ )
55 54 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( 𝑦 − 𝑟 ) ∈ ℝ* )
56 elioopnf ⊢ ( ( 𝑦 − 𝑟 ) ∈ ℝ* → ( ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ↔ ( ( 𝐺 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑦 − 𝑟 ) < ( 𝐺 ‘ 𝑥 ) ) ) )
57 55 56 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ↔ ( ( 𝐺 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑦 − 𝑟 ) < ( 𝐺 ‘ 𝑥 ) ) ) )
58 24 57 mpbirand ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ↔ ( 𝑦 − 𝑟 ) < ( 𝐺 ‘ 𝑥 ) ) )
59 53 58 anbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑟 ∈ ℚ ) → ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ↔ ( 𝑟 < ( 𝐹 ‘ 𝑥 ) ∧ ( 𝑦 − 𝑟 ) < ( 𝐺 ‘ 𝑥 ) ) ) )
60 59 rexbidva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ ℚ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ↔ ∃ 𝑟 ∈ ℚ ( 𝑟 < ( 𝐹 ‘ 𝑥 ) ∧ ( 𝑦 − 𝑟 ) < ( 𝐺 ‘ 𝑥 ) ) ) )
61 12 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ∘f + 𝐺 ) : 𝐴 ⟶ ℝ )
62 61 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ∈ ℝ )
63 15 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
64 elioopnf ⊢ ( 𝑦 ∈ ℝ* → ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ∈ ℝ ∧ 𝑦 < ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ) ) )
65 63 64 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ∈ ℝ ∧ 𝑦 < ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ) ) )
66 62 65 mpbirand ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ↔ 𝑦 < ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ) )
67 49 60 66 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ ℚ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ↔ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) )
68 67 pm5.32da ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑟 ∈ ℚ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
69 14 68 bitrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑟 ∈ ℚ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
70 elpreima ⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ) ) )
71 41 70 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ) ) )
72 elpreima ⊢ ( 𝐺 Fn 𝐴 → ( 𝑥 ∈ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) )
73 43 72 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) )
74 71 73 anbi12d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ) )
75 elin ⊢ ( 𝑥 ∈ ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ↔ ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) )
76 anandi ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) )
77 74 75 76 3bitr4g ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ∈ ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ) )
78 77 rexbidv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑟 ∈ ℚ 𝑥 ∈ ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ↔ ∃ 𝑟 ∈ ℚ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑟 (,) +∞ ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ) )
79 12 ffnd ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) Fn 𝐴 )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ∘f + 𝐺 ) Fn 𝐴 )
81 elpreima ⊢ ( ( 𝐹 ∘f + 𝐺 ) Fn 𝐴 → ( 𝑥 ∈ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
82 80 81 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
83 69 78 82 3bitr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑟 ∈ ℚ 𝑥 ∈ ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ↔ 𝑥 ∈ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑦 (,) +∞ ) ) ) )
84 13 83 bitrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ∈ ∪ 𝑟 ∈ ℚ ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ↔ 𝑥 ∈ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑦 (,) +∞ ) ) ) )
85 84 eqrdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∪ 𝑟 ∈ ℚ ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) = ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑦 (,) +∞ ) ) )
86 qnnen ⊢ ℚ ≈ ℕ
87 endom ⊢ ( ℚ ≈ ℕ → ℚ ≼ ℕ )
88 86 87 ax-mp ⊢ ℚ ≼ ℕ
89 mbfima ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∈ dom vol )
90 1 3 89 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∈ dom vol )
91 mbfima ⊢ ( ( 𝐺 ∈ MblFn ∧ 𝐺 : 𝐴 ⟶ ℝ ) → ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ∈ dom vol )
92 2 4 91 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ∈ dom vol )
93 inmbl ⊢ ( ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∈ dom vol ∧ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ∈ dom vol ) → ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ∈ dom vol )
94 90 92 93 syl2anc ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ∈ dom vol )
95 94 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℚ ) → ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ∈ dom vol )
96 95 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∀ 𝑟 ∈ ℚ ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ∈ dom vol )
97 iunmbl2 ⊢ ( ( ℚ ≼ ℕ ∧ ∀ 𝑟 ∈ ℚ ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ∈ dom vol ) → ∪ 𝑟 ∈ ℚ ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ∈ dom vol )
98 88 96 97 sylancr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∪ 𝑟 ∈ ℚ ( ( ◡ 𝐹 “ ( 𝑟 (,) +∞ ) ) ∩ ( ◡ 𝐺 “ ( ( 𝑦 − 𝑟 ) (,) +∞ ) ) ) ∈ dom vol )
99 85 98 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
100 12 99 ismbf3d ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ MblFn )