This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
7 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
8 6 7 ifcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
9 8 5 fmptd ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ ℝ )
10 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → 𝐹 : 𝐴 ⟶ ℝ )
11 10 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
12 11 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ* )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → 𝐺 : 𝐴 ⟶ ℝ )
14 13 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℝ )
15 14 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℝ* )
16 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
17 xrmaxle ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ* ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ↔ ( ( 𝐹 ‘ 𝑧 ) ≤ 𝑦 ∧ ( 𝐺 ‘ 𝑧 ) ≤ 𝑦 ) ) )
18 12 15 16 17 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ↔ ( ( 𝐹 ‘ 𝑧 ) ≤ 𝑦 ∧ ( 𝐺 ‘ 𝑧 ) ≤ 𝑦 ) ) )
19 18 notbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( ¬ if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) , ( 𝐹 ‘ 𝑧 ) ) ≤ 𝑦 ↔ ¬ ( ( 𝐹 ‘ 𝑧 ) ≤ 𝑦 ∧ ( 𝐺 ‘ 𝑧 ) ≤ 𝑦 ) ) )
20 ianor ⊢ ( ¬ ( ( 𝐹 ‘ 𝑧 ) ≤ 𝑦 ∧ ( 𝐺 ‘ 𝑧 ) ≤ 𝑦 ) ↔ ( ¬ ( 𝐹 ‘ 𝑧 ) ≤ 𝑦 ∨ ¬ ( 𝐺 ‘ 𝑧 ) ≤ 𝑦 ) )
21 19 20 bitrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( ¬ 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 bitrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( 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 bitrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( 𝑦 < ( 𝐹 ‘ 𝑧 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) < +∞ ) ) ) )
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 bitrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( 𝑦 < ( 𝐺 ‘ 𝑧 ) ∧ ( ( 𝐺 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) < +∞ ) ) ) )
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 bitrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑧 ∈ 𝐴 ∧ ( 𝐻 ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ∨ ( 𝑧 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) ) )
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 bitr4di ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( ◡ 𝐻 “ ( 𝑦 (,) +∞ ) ) ↔ 𝑧 ∈ ( ( ◡ 𝐹 “ ( 𝑦 (,) +∞ ) ) ∪ ( ◡ 𝐺 “ ( 𝑦 (,) +∞ ) ) ) ) )
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 bitrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( 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 bitrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐹 ‘ 𝑧 ) ) ∧ ( 𝐹 ‘ 𝑧 ) < 𝑦 ) ) )
112 107 111 mpbirand ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) < 𝑦 ) )
113 mnflt ⊢ ( ( 𝐺 ‘ 𝑧 ) ∈ ℝ → -∞ < ( 𝐺 ‘ 𝑧 ) )
114 14 113 jccir ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐺 ‘ 𝑧 ) ) )
115 elioo2 ⊢ ( ( -∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝐺 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( 𝐺 ‘ 𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐺 ‘ 𝑧 ) ∧ ( 𝐺 ‘ 𝑧 ) < 𝑦 ) ) )
116 96 16 115 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( 𝐺 ‘ 𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐺 ‘ 𝑧 ) ∧ ( 𝐺 ‘ 𝑧 ) < 𝑦 ) ) )
117 df-3an ⊢ ( ( ( 𝐺 ‘ 𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐺 ‘ 𝑧 ) ∧ ( 𝐺 ‘ 𝑧 ) < 𝑦 ) ↔ ( ( ( 𝐺 ‘ 𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐺 ‘ 𝑧 ) ) ∧ ( 𝐺 ‘ 𝑧 ) < 𝑦 ) )
118 116 117 bitrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( ( 𝐺 ‘ 𝑧 ) ∈ ℝ ∧ -∞ < ( 𝐺 ‘ 𝑧 ) ) ∧ ( 𝐺 ‘ 𝑧 ) < 𝑦 ) ) )
119 114 118 mpbirand ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( 𝐺 ‘ 𝑧 ) < 𝑦 ) )
120 112 119 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) < 𝑦 ∧ ( 𝐺 ‘ 𝑧 ) < 𝑦 ) ) )
121 95 105 120 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
122 121 pm5.32da ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑧 ∈ 𝐴 ∧ ( 𝐻 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) ) )
123 anandi ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
124 122 123 bitrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑧 ∈ 𝐴 ∧ ( 𝐻 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) ) )
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 bitr4di ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ* ) → ( 𝑧 ∈ ( ◡ 𝐻 “ ( -∞ (,) 𝑦 ) ) ↔ 𝑧 ∈ ( ( ◡ 𝐹 “ ( -∞ (,) 𝑦 ) ) ∩ ( ◡ 𝐺 “ ( -∞ (,) 𝑦 ) ) ) ) )
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 )