Metamath Proof Explorer


Theorem mbfmax

Description: The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses mbfmax.1 ( 𝜑𝐹 : 𝐴 ⟶ ℝ )
mbfmax.2 ( 𝜑𝐹 ∈ MblFn )
mbfmax.3 ( 𝜑𝐺 : 𝐴 ⟶ ℝ )
mbfmax.4 ( 𝜑𝐺 ∈ MblFn )
mbfmax.5 𝐻 = ( 𝑥𝐴 ↦ if ( ( 𝐹𝑥 ) ≤ ( 𝐺𝑥 ) , ( 𝐺𝑥 ) , ( 𝐹𝑥 ) ) )
Assertion mbfmax ( 𝜑𝐻 ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfmax.1 ( 𝜑𝐹 : 𝐴 ⟶ ℝ )
2 mbfmax.2 ( 𝜑𝐹 ∈ MblFn )
3 mbfmax.3 ( 𝜑𝐺 : 𝐴 ⟶ ℝ )
4 mbfmax.4 ( 𝜑𝐺 ∈ MblFn )
5 mbfmax.5 𝐻 = ( 𝑥𝐴 ↦ if ( ( 𝐹𝑥 ) ≤ ( 𝐺𝑥 ) , ( 𝐺𝑥 ) , ( 𝐹𝑥 ) ) )
6 3 ffvelrnda ( ( 𝜑𝑥𝐴 ) → ( 𝐺𝑥 ) ∈ ℝ )
7 1 ffvelrnda ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ℝ )
8 6 7 ifcld ( ( 𝜑𝑥𝐴 ) → if ( ( 𝐹𝑥 ) ≤ ( 𝐺𝑥 ) , ( 𝐺𝑥 ) , ( 𝐹𝑥 ) ) ∈ ℝ )
9 8 5 fmptd ( 𝜑𝐻 : 𝐴 ⟶ ℝ )
10 1 adantr ( ( 𝜑𝑦 ∈ ℝ* ) → 𝐹 : 𝐴 ⟶ ℝ )
11 10 ffvelrnda ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( 𝐹𝑧 ) ∈ ℝ )
12 11 rexrd ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( 𝐹𝑧 ) ∈ ℝ* )
13 3 adantr ( ( 𝜑𝑦 ∈ ℝ* ) → 𝐺 : 𝐴 ⟶ ℝ )
14 13 ffvelrnda ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( 𝐺𝑧 ) ∈ ℝ )
15 14 rexrd ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( 𝐺𝑧 ) ∈ ℝ* )
16 simplr ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → 𝑦 ∈ ℝ* )
17 xrmaxle ( ( ( 𝐹𝑧 ) ∈ ℝ* ∧ ( 𝐺𝑧 ) ∈ ℝ*𝑦 ∈ ℝ* ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ≤ 𝑦 ↔ ( ( 𝐹𝑧 ) ≤ 𝑦 ∧ ( 𝐺𝑧 ) ≤ 𝑦 ) ) )
18 12 15 16 17 syl3anc ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ≤ 𝑦 ↔ ( ( 𝐹𝑧 ) ≤ 𝑦 ∧ ( 𝐺𝑧 ) ≤ 𝑦 ) ) )
19 18 notbid ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ¬ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ≤ 𝑦 ↔ ¬ ( ( 𝐹𝑧 ) ≤ 𝑦 ∧ ( 𝐺𝑧 ) ≤ 𝑦 ) ) )
20 ianor ( ¬ ( ( 𝐹𝑧 ) ≤ 𝑦 ∧ ( 𝐺𝑧 ) ≤ 𝑦 ) ↔ ( ¬ ( 𝐹𝑧 ) ≤ 𝑦 ∨ ¬ ( 𝐺𝑧 ) ≤ 𝑦 ) )
21 19 20 syl6bb ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ¬ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ≤ 𝑦 ↔ ( ¬ ( 𝐹𝑧 ) ≤ 𝑦 ∨ ¬ ( 𝐺𝑧 ) ≤ 𝑦 ) ) )
22 pnfxr +∞ ∈ ℝ*
23 elioo2 ( ( 𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ( 𝑦 (,) +∞ ) ↔ ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ 𝑦 < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < +∞ ) ) )
24 16 22 23 sylancl ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ( 𝑦 (,) +∞ ) ↔ ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ 𝑦 < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < +∞ ) ) )
25 3anan12 ( ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ 𝑦 < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < +∞ ) ↔ ( 𝑦 < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∧ ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < +∞ ) ) )
26 24 25 syl6bb ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ( 𝑦 (,) +∞ ) ↔ ( 𝑦 < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∧ ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < +∞ ) ) ) )
27 fveq2 ( 𝑥 = 𝑧 → ( 𝐹𝑥 ) = ( 𝐹𝑧 ) )
28 fveq2 ( 𝑥 = 𝑧 → ( 𝐺𝑥 ) = ( 𝐺𝑧 ) )
29 27 28 breq12d ( 𝑥 = 𝑧 → ( ( 𝐹𝑥 ) ≤ ( 𝐺𝑥 ) ↔ ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) ) )
30 29 28 27 ifbieq12d ( 𝑥 = 𝑧 → if ( ( 𝐹𝑥 ) ≤ ( 𝐺𝑥 ) , ( 𝐺𝑥 ) , ( 𝐹𝑥 ) ) = if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) )
31 fvex ( 𝐺𝑧 ) ∈ V
32 fvex ( 𝐹𝑧 ) ∈ V
33 31 32 ifex if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ V
34 30 5 33 fvmpt ( 𝑧𝐴 → ( 𝐻𝑧 ) = if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) )
35 34 adantl ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( 𝐻𝑧 ) = if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) )
36 35 eleq1d ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐻𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ( 𝑦 (,) +∞ ) ) )
37 14 11 ifcld ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ )
38 ltpnf ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ → if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < +∞ )
39 37 38 jccir ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < +∞ ) )
40 39 biantrud ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( 𝑦 < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ↔ ( 𝑦 < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∧ ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < +∞ ) ) ) )
41 26 36 40 3bitr4d ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐻𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ 𝑦 < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ) )
42 37 rexrd ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ* )
43 xrltnle ( ( 𝑦 ∈ ℝ* ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ* ) → ( 𝑦 < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ↔ ¬ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ≤ 𝑦 ) )
44 16 42 43 syl2anc ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( 𝑦 < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ↔ ¬ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ≤ 𝑦 ) )
45 41 44 bitrd ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐻𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ¬ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ≤ 𝑦 ) )
46 elioo2 ( ( 𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( 𝐹𝑧 ) ∈ ℝ ∧ 𝑦 < ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) < +∞ ) ) )
47 16 22 46 sylancl ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( 𝐹𝑧 ) ∈ ℝ ∧ 𝑦 < ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) < +∞ ) ) )
48 3anan12 ( ( ( 𝐹𝑧 ) ∈ ℝ ∧ 𝑦 < ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) < +∞ ) ↔ ( 𝑦 < ( 𝐹𝑧 ) ∧ ( ( 𝐹𝑧 ) ∈ ℝ ∧ ( 𝐹𝑧 ) < +∞ ) ) )
49 47 48 syl6bb ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( 𝑦 < ( 𝐹𝑧 ) ∧ ( ( 𝐹𝑧 ) ∈ ℝ ∧ ( 𝐹𝑧 ) < +∞ ) ) ) )
50 ltpnf ( ( 𝐹𝑧 ) ∈ ℝ → ( 𝐹𝑧 ) < +∞ )
51 11 50 jccir ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐹𝑧 ) ∈ ℝ ∧ ( 𝐹𝑧 ) < +∞ ) )
52 51 biantrud ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( 𝑦 < ( 𝐹𝑧 ) ↔ ( 𝑦 < ( 𝐹𝑧 ) ∧ ( ( 𝐹𝑧 ) ∈ ℝ ∧ ( 𝐹𝑧 ) < +∞ ) ) ) )
53 xrltnle ( ( 𝑦 ∈ ℝ* ∧ ( 𝐹𝑧 ) ∈ ℝ* ) → ( 𝑦 < ( 𝐹𝑧 ) ↔ ¬ ( 𝐹𝑧 ) ≤ 𝑦 ) )
54 16 12 53 syl2anc ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( 𝑦 < ( 𝐹𝑧 ) ↔ ¬ ( 𝐹𝑧 ) ≤ 𝑦 ) )
55 49 52 54 3bitr2d ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ¬ ( 𝐹𝑧 ) ≤ 𝑦 ) )
56 elioo2 ( ( 𝑦 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( 𝐺𝑧 ) ∈ ℝ ∧ 𝑦 < ( 𝐺𝑧 ) ∧ ( 𝐺𝑧 ) < +∞ ) ) )
57 16 22 56 sylancl ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( 𝐺𝑧 ) ∈ ℝ ∧ 𝑦 < ( 𝐺𝑧 ) ∧ ( 𝐺𝑧 ) < +∞ ) ) )
58 3anan12 ( ( ( 𝐺𝑧 ) ∈ ℝ ∧ 𝑦 < ( 𝐺𝑧 ) ∧ ( 𝐺𝑧 ) < +∞ ) ↔ ( 𝑦 < ( 𝐺𝑧 ) ∧ ( ( 𝐺𝑧 ) ∈ ℝ ∧ ( 𝐺𝑧 ) < +∞ ) ) )
59 57 58 syl6bb ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( 𝑦 < ( 𝐺𝑧 ) ∧ ( ( 𝐺𝑧 ) ∈ ℝ ∧ ( 𝐺𝑧 ) < +∞ ) ) ) )
60 ltpnf ( ( 𝐺𝑧 ) ∈ ℝ → ( 𝐺𝑧 ) < +∞ )
61 14 60 jccir ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐺𝑧 ) ∈ ℝ ∧ ( 𝐺𝑧 ) < +∞ ) )
62 61 biantrud ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( 𝑦 < ( 𝐺𝑧 ) ↔ ( 𝑦 < ( 𝐺𝑧 ) ∧ ( ( 𝐺𝑧 ) ∈ ℝ ∧ ( 𝐺𝑧 ) < +∞ ) ) ) )
63 xrltnle ( ( 𝑦 ∈ ℝ* ∧ ( 𝐺𝑧 ) ∈ ℝ* ) → ( 𝑦 < ( 𝐺𝑧 ) ↔ ¬ ( 𝐺𝑧 ) ≤ 𝑦 ) )
64 16 15 63 syl2anc ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( 𝑦 < ( 𝐺𝑧 ) ↔ ¬ ( 𝐺𝑧 ) ≤ 𝑦 ) )
65 59 62 64 3bitr2d ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ¬ ( 𝐺𝑧 ) ≤ 𝑦 ) )
66 55 65 orbi12d ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ∨ ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ↔ ( ¬ ( 𝐹𝑧 ) ≤ 𝑦 ∨ ¬ ( 𝐺𝑧 ) ≤ 𝑦 ) ) )
67 21 45 66 3bitr4d ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐻𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ∨ ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
68 67 pm5.32da ( ( 𝜑𝑦 ∈ ℝ* ) → ( ( 𝑧𝐴 ∧ ( 𝐻𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧𝐴 ∧ ( ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ∨ ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) ) )
69 andi ( ( 𝑧𝐴 ∧ ( ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ∨ ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) ↔ ( ( 𝑧𝐴 ∧ ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ∨ ( 𝑧𝐴 ∧ ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
70 68 69 syl6bb ( ( 𝜑𝑦 ∈ ℝ* ) → ( ( 𝑧𝐴 ∧ ( 𝐻𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ↔ ( ( 𝑧𝐴 ∧ ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ∨ ( 𝑧𝐴 ∧ ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) ) )
71 9 ffnd ( 𝜑𝐻 Fn 𝐴 )
72 71 adantr ( ( 𝜑𝑦 ∈ ℝ* ) → 𝐻 Fn 𝐴 )
73 elpreima ( 𝐻 Fn 𝐴 → ( 𝑧 ∈ ( 𝐻 “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧𝐴 ∧ ( 𝐻𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
74 72 73 syl ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝐻 “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧𝐴 ∧ ( 𝐻𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
75 10 ffnd ( ( 𝜑𝑦 ∈ ℝ* ) → 𝐹 Fn 𝐴 )
76 elpreima ( 𝐹 Fn 𝐴 → ( 𝑧 ∈ ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧𝐴 ∧ ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
77 75 76 syl ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧𝐴 ∧ ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
78 13 ffnd ( ( 𝜑𝑦 ∈ ℝ* ) → 𝐺 Fn 𝐴 )
79 elpreima ( 𝐺 Fn 𝐴 → ( 𝑧 ∈ ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧𝐴 ∧ ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
80 78 79 syl ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧𝐴 ∧ ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
81 77 80 orbi12d ( ( 𝜑𝑦 ∈ ℝ* ) → ( ( 𝑧 ∈ ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ∨ 𝑧 ∈ ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ) ↔ ( ( 𝑧𝐴 ∧ ( 𝐹𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ∨ ( 𝑧𝐴 ∧ ( 𝐺𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) ) )
82 70 74 81 3bitr4d ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝐻 “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧 ∈ ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ∨ 𝑧 ∈ ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ) ) )
83 elun ( 𝑧 ∈ ( ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ∪ ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ) ↔ ( 𝑧 ∈ ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ∨ 𝑧 ∈ ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ) )
84 82 83 syl6bbr ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝐻 “ ( 𝑦 (,) +∞ ) ) ↔ 𝑧 ∈ ( ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ∪ ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ) ) )
85 84 eqrdv ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝐻 “ ( 𝑦 (,) +∞ ) ) = ( ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ∪ ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ) )
86 mbfima ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
87 2 1 86 syl2anc ( 𝜑 → ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
88 mbfima ( ( 𝐺 ∈ MblFn ∧ 𝐺 : 𝐴 ⟶ ℝ ) → ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
89 4 3 88 syl2anc ( 𝜑 → ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
90 unmbl ( ( ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ∈ dom vol ∧ ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ∈ dom vol ) → ( ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ∪ ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ) ∈ dom vol )
91 87 89 90 syl2anc ( 𝜑 → ( ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ∪ ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ) ∈ dom vol )
92 91 adantr ( ( 𝜑𝑦 ∈ ℝ* ) → ( ( 𝐹 “ ( 𝑦 (,) +∞ ) ) ∪ ( 𝐺 “ ( 𝑦 (,) +∞ ) ) ) ∈ dom vol )
93 85 92 eqeltrd ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝐻 “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
94 xrmaxlt ( ( ( 𝐹𝑧 ) ∈ ℝ* ∧ ( 𝐺𝑧 ) ∈ ℝ*𝑦 ∈ ℝ* ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < 𝑦 ↔ ( ( 𝐹𝑧 ) < 𝑦 ∧ ( 𝐺𝑧 ) < 𝑦 ) ) )
95 12 15 16 94 syl3anc ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < 𝑦 ↔ ( ( 𝐹𝑧 ) < 𝑦 ∧ ( 𝐺𝑧 ) < 𝑦 ) ) )
96 mnfxr -∞ ∈ ℝ*
97 elioo2 ( ( -∞ ∈ ℝ*𝑦 ∈ ℝ* ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ( -∞ (,) 𝑦 ) ↔ ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ -∞ < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < 𝑦 ) ) )
98 96 16 97 sylancr ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ( -∞ (,) 𝑦 ) ↔ ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ -∞ < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < 𝑦 ) ) )
99 df-3an ( ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ -∞ < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < 𝑦 ) ↔ ( ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ -∞ < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ) ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < 𝑦 ) )
100 98 99 syl6bb ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ -∞ < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ) ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < 𝑦 ) ) )
101 35 eleq1d ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐻𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ( -∞ (,) 𝑦 ) ) )
102 mnflt ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ → -∞ < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) )
103 37 102 jccir ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ -∞ < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ) )
104 103 biantrurd ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < 𝑦 ↔ ( ( if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ∈ ℝ ∧ -∞ < if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) ) ∧ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < 𝑦 ) ) )
105 100 101 104 3bitr4d ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐻𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ if ( ( 𝐹𝑧 ) ≤ ( 𝐺𝑧 ) , ( 𝐺𝑧 ) , ( 𝐹𝑧 ) ) < 𝑦 ) )
106 mnflt ( ( 𝐹𝑧 ) ∈ ℝ → -∞ < ( 𝐹𝑧 ) )
107 11 106 jccir ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐹𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐹𝑧 ) ) )
108 elioo2 ( ( -∞ ∈ ℝ*𝑦 ∈ ℝ* ) → ( ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( 𝐹𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) < 𝑦 ) ) )
109 96 16 108 sylancr ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( 𝐹𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) < 𝑦 ) ) )
110 df-3an ( ( ( 𝐹𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐹𝑧 ) ∧ ( 𝐹𝑧 ) < 𝑦 ) ↔ ( ( ( 𝐹𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐹𝑧 ) ) ∧ ( 𝐹𝑧 ) < 𝑦 ) )
111 109 110 syl6bb ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( ( 𝐹𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐹𝑧 ) ) ∧ ( 𝐹𝑧 ) < 𝑦 ) ) )
112 107 111 mpbirand ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( 𝐹𝑧 ) < 𝑦 ) )
113 mnflt ( ( 𝐺𝑧 ) ∈ ℝ → -∞ < ( 𝐺𝑧 ) )
114 14 113 jccir ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐺𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐺𝑧 ) ) )
115 elioo2 ( ( -∞ ∈ ℝ*𝑦 ∈ ℝ* ) → ( ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( 𝐺𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐺𝑧 ) ∧ ( 𝐺𝑧 ) < 𝑦 ) ) )
116 96 16 115 sylancr ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( 𝐺𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐺𝑧 ) ∧ ( 𝐺𝑧 ) < 𝑦 ) ) )
117 df-3an ( ( ( 𝐺𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐺𝑧 ) ∧ ( 𝐺𝑧 ) < 𝑦 ) ↔ ( ( ( 𝐺𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐺𝑧 ) ) ∧ ( 𝐺𝑧 ) < 𝑦 ) )
118 116 117 syl6bb ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( ( 𝐺𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐺𝑧 ) ) ∧ ( 𝐺𝑧 ) < 𝑦 ) ) )
119 114 118 mpbirand ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( 𝐺𝑧 ) < 𝑦 ) )
120 112 119 anbi12d ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ∧ ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ↔ ( ( 𝐹𝑧 ) < 𝑦 ∧ ( 𝐺𝑧 ) < 𝑦 ) ) )
121 95 105 120 3bitr4d ( ( ( 𝜑𝑦 ∈ ℝ* ) ∧ 𝑧𝐴 ) → ( ( 𝐻𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ∧ ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
122 121 pm5.32da ( ( 𝜑𝑦 ∈ ℝ* ) → ( ( 𝑧𝐴 ∧ ( 𝐻𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧𝐴 ∧ ( ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ∧ ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) ) )
123 anandi ( ( 𝑧𝐴 ∧ ( ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ∧ ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) ↔ ( ( 𝑧𝐴 ∧ ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
124 122 123 syl6bb ( ( 𝜑𝑦 ∈ ℝ* ) → ( ( 𝑧𝐴 ∧ ( 𝐻𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ↔ ( ( 𝑧𝐴 ∧ ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) ) )
125 elpreima ( 𝐻 Fn 𝐴 → ( 𝑧 ∈ ( 𝐻 “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧𝐴 ∧ ( 𝐻𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
126 72 125 syl ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝐻 “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧𝐴 ∧ ( 𝐻𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
127 elpreima ( 𝐹 Fn 𝐴 → ( 𝑧 ∈ ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧𝐴 ∧ ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
128 75 127 syl ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧𝐴 ∧ ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
129 elpreima ( 𝐺 Fn 𝐴 → ( 𝑧 ∈ ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧𝐴 ∧ ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
130 78 129 syl ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧𝐴 ∧ ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
131 128 130 anbi12d ( ( 𝜑𝑦 ∈ ℝ* ) → ( ( 𝑧 ∈ ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ) ↔ ( ( 𝑧𝐴 ∧ ( 𝐹𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ∧ ( 𝑧𝐴 ∧ ( 𝐺𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) ) )
132 124 126 131 3bitr4d ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝐻 “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧 ∈ ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ) ) )
133 elin ( 𝑧 ∈ ( ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ∩ ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ) ↔ ( 𝑧 ∈ ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ) )
134 132 133 syl6bbr ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝐻 “ ( -∞ (,) 𝑦 ) ) ↔ 𝑧 ∈ ( ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ∩ ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ) ) )
135 134 eqrdv ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝐻 “ ( -∞ (,) 𝑦 ) ) = ( ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ∩ ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ) )
136 mbfima ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
137 2 1 136 syl2anc ( 𝜑 → ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
138 mbfima ( ( 𝐺 ∈ MblFn ∧ 𝐺 : 𝐴 ⟶ ℝ ) → ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
139 4 3 138 syl2anc ( 𝜑 → ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
140 inmbl ( ( ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ∈ dom vol ∧ ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ∈ dom vol ) → ( ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ∩ ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ) ∈ dom vol )
141 137 139 140 syl2anc ( 𝜑 → ( ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ∩ ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ) ∈ dom vol )
142 141 adantr ( ( 𝜑𝑦 ∈ ℝ* ) → ( ( 𝐹 “ ( -∞ (,) 𝑦 ) ) ∩ ( 𝐺 “ ( -∞ (,) 𝑦 ) ) ) ∈ dom vol )
143 135 142 eqeltrd ( ( 𝜑𝑦 ∈ ℝ* ) → ( 𝐻 “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
144 9 93 143 ismbfd ( 𝜑𝐻 ∈ MblFn )