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

Metamath Proof Explorer

Theorem mbfposr

Description: Converse to mbfpos . (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses mbfpos.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
mbfposr.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn )
mbfposr.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn )
Assertion mbfposr ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfpos.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
2 mbfposr.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn )
3 mbfposr.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn )
4 1 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )
5 0re ⊢ 0 ∈ ℝ
6 ifcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
7 1 5 6 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
8 2 7 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
9 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 < 0 )
10 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
11 10 lt0neg1d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < 0 ↔ 0 < - 𝑦 ) )
12 9 11 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → 0 < - 𝑦 )
13 12 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 < - 𝑦 ↔ ( 0 < - 𝑦 ∧ - 𝐵 < - 𝑦 ) ) )
14 1 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
15 10 14 ltnegd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < 𝐵 ↔ - 𝐵 < - 𝑦 ) )
16 0red ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ ℝ )
17 14 renegcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
18 10 renegcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → - 𝑦 ∈ ℝ )
19 maxlt ⊢ ( ( 0 ∈ ℝ ∧ - 𝐵 ∈ ℝ ∧ - 𝑦 ∈ ℝ ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) < - 𝑦 ↔ ( 0 < - 𝑦 ∧ - 𝐵 < - 𝑦 ) ) )
20 16 17 18 19 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) < - 𝑦 ↔ ( 0 < - 𝑦 ∧ - 𝐵 < - 𝑦 ) ) )
21 13 15 20 3bitr4rd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) < - 𝑦 ↔ 𝑦 < 𝐵 ) )
22 1 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
23 ifcl ⊢ ( ( - 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ )
24 22 5 23 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ )
25 24 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ )
26 25 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) < - 𝑦 ↔ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ ∧ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) < - 𝑦 ) ) )
27 14 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < 𝐵 ↔ ( 𝐵 ∈ ℝ ∧ 𝑦 < 𝐵 ) ) )
28 21 26 27 3bitr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ ∧ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) < - 𝑦 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑦 < 𝐵 ) ) )
29 18 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → - 𝑦 ∈ ℝ* )
30 elioomnf ⊢ ( - 𝑦 ∈ ℝ* → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ( -∞ (,) - 𝑦 ) ↔ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ ∧ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) < - 𝑦 ) ) )
31 29 30 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ( -∞ (,) - 𝑦 ) ↔ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ ∧ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) < - 𝑦 ) ) )
32 10 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
33 elioopnf ⊢ ( 𝑦 ∈ ℝ* → ( 𝐵 ∈ ( 𝑦 (,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑦 < 𝐵 ) ) )
34 32 33 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ∈ ( 𝑦 (,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑦 < 𝐵 ) ) )
35 28 31 34 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ( -∞ (,) - 𝑦 ) ↔ 𝐵 ∈ ( 𝑦 (,) +∞ ) ) )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
37 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
38 37 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) = if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
39 36 24 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) = if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
40 39 eleq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) - 𝑦 ) ↔ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ( -∞ (,) - 𝑦 ) ) )
41 40 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) - 𝑦 ) ↔ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ( -∞ (,) - 𝑦 ) ) )
42 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
43 42 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
44 36 1 43 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
45 44 eleq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ↔ 𝐵 ∈ ( 𝑦 (,) +∞ ) ) )
46 45 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ↔ 𝐵 ∈ ( 𝑦 (,) +∞ ) ) )
47 35 41 46 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) - 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) )
48 47 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) → ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) - 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
49 24 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) : 𝐴 ⟶ ℝ )
50 ffn ⊢ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) : 𝐴 ⟶ ℝ → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) Fn 𝐴 )
51 elpreima ⊢ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) Fn 𝐴 → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( -∞ (,) - 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) - 𝑦 ) ) ) )
52 49 50 51 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( -∞ (,) - 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) - 𝑦 ) ) ) )
53 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( -∞ (,) - 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) - 𝑦 ) ) ) )
54 ffn ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
55 elpreima ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
56 4 54 55 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
57 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
58 48 53 57 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( -∞ (,) - 𝑦 ) ) ↔ 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ) )
59 58 alrimiv ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) → ∀ 𝑥 ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( -∞ (,) - 𝑦 ) ) ↔ 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ) )
60 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
61 60 nfcnv ⊢ Ⅎ 𝑥 ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
62 nfcv ⊢ Ⅎ 𝑥 ( -∞ (,) - 𝑦 )
63 61 62 nfima ⊢ Ⅎ 𝑥 ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( -∞ (,) - 𝑦 ) )
64 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
65 64 nfcnv ⊢ Ⅎ 𝑥 ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
66 nfcv ⊢ Ⅎ 𝑥 ( 𝑦 (,) +∞ )
67 65 66 nfima ⊢ Ⅎ 𝑥 ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) )
68 63 67 cleqf ⊢ ( ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( -∞ (,) - 𝑦 ) ) = ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( -∞ (,) - 𝑦 ) ) ↔ 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ) )
69 59 68 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( -∞ (,) - 𝑦 ) ) = ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) )
70 mbfima ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) : 𝐴 ⟶ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( -∞ (,) - 𝑦 ) ) ∈ dom vol )
71 3 49 70 syl2anc ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( -∞ (,) - 𝑦 ) ) ∈ dom vol )
72 71 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( -∞ (,) - 𝑦 ) ) ∈ dom vol )
73 69 72 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 < 0 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
74 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝑦 )
75 0red ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ ℝ )
76 1 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
77 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
78 maxle ⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ≤ 𝑦 ↔ ( 0 ≤ 𝑦 ∧ 𝐵 ≤ 𝑦 ) ) )
79 75 76 77 78 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ≤ 𝑦 ↔ ( 0 ≤ 𝑦 ∧ 𝐵 ≤ 𝑦 ) ) )
80 74 79 mpbirand ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ≤ 𝑦 ↔ 𝐵 ≤ 𝑦 ) )
81 80 notbid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ≤ 𝑦 ↔ ¬ 𝐵 ≤ 𝑦 ) )
82 76 5 6 sylancl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
83 77 82 ltnled ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ↔ ¬ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ≤ 𝑦 ) )
84 77 76 ltnled ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < 𝐵 ↔ ¬ 𝐵 ≤ 𝑦 ) )
85 81 83 84 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ↔ 𝑦 < 𝐵 ) )
86 82 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ↔ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ ∧ 𝑦 < if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) )
87 76 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 < 𝐵 ↔ ( 𝐵 ∈ ℝ ∧ 𝑦 < 𝐵 ) ) )
88 85 86 87 3bitr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ ∧ 𝑦 < if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑦 < 𝐵 ) ) )
89 77 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
90 elioopnf ⊢ ( 𝑦 ∈ ℝ* → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ ∧ 𝑦 < if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) )
91 89 90 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ ∧ 𝑦 < if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) )
92 89 33 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ∈ ( 𝑦 (,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 𝑦 < 𝐵 ) ) )
93 88 91 92 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( 𝑦 (,) +∞ ) ↔ 𝐵 ∈ ( 𝑦 (,) +∞ ) ) )
94 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
95 94 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
96 36 7 95 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
97 96 eleq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ↔ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( 𝑦 (,) +∞ ) ) )
98 97 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ↔ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( 𝑦 (,) +∞ ) ) )
99 45 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ↔ 𝐵 ∈ ( 𝑦 (,) +∞ ) ) )
100 93 98 99 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) )
101 100 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) → ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
102 7 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) : 𝐴 ⟶ ℝ )
103 ffn ⊢ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) : 𝐴 ⟶ ℝ → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) Fn 𝐴 )
104 elpreima ⊢ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) Fn 𝐴 → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
105 102 103 104 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
106 105 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
107 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
108 101 106 107 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( 𝑦 (,) +∞ ) ) ↔ 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ) )
109 108 alrimiv ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( 𝑦 (,) +∞ ) ) ↔ 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ) )
110 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
111 110 nfcnv ⊢ Ⅎ 𝑥 ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
112 111 66 nfima ⊢ Ⅎ 𝑥 ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( 𝑦 (,) +∞ ) )
113 112 67 cleqf ⊢ ( ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( 𝑦 (,) +∞ ) ) = ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( 𝑦 (,) +∞ ) ) ↔ 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ) )
114 109 113 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( 𝑦 (,) +∞ ) ) = ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) )
115 mbfima ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) : 𝐴 ⟶ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
116 2 102 115 syl2anc ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
117 116 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
118 114 117 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 ≤ 𝑦 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
119 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
120 0red ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 0 ∈ ℝ )
121 73 118 119 120 ltlecasei ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
122 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 0 < 𝑦 )
123 0red ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ ℝ )
124 1 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
125 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
126 maxlt ⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) < 𝑦 ↔ ( 0 < 𝑦 ∧ 𝐵 < 𝑦 ) ) )
127 123 124 125 126 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) < 𝑦 ↔ ( 0 < 𝑦 ∧ 𝐵 < 𝑦 ) ) )
128 122 127 mpbirand ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) < 𝑦 ↔ 𝐵 < 𝑦 ) )
129 7 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
130 129 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) < 𝑦 ↔ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ ∧ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) < 𝑦 ) ) )
131 124 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 < 𝑦 ↔ ( 𝐵 ∈ ℝ ∧ 𝐵 < 𝑦 ) ) )
132 128 130 131 3bitr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ ∧ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) < 𝑦 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐵 < 𝑦 ) ) )
133 125 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
134 elioomnf ⊢ ( 𝑦 ∈ ℝ* → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ ∧ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) < 𝑦 ) ) )
135 133 134 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ ∧ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) < 𝑦 ) ) )
136 elioomnf ⊢ ( 𝑦 ∈ ℝ* → ( 𝐵 ∈ ( -∞ (,) 𝑦 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐵 < 𝑦 ) ) )
137 133 136 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ∈ ( -∞ (,) 𝑦 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐵 < 𝑦 ) ) )
138 132 135 137 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( -∞ (,) 𝑦 ) ↔ 𝐵 ∈ ( -∞ (,) 𝑦 ) ) )
139 96 eleq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ↔ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( -∞ (,) 𝑦 ) ) )
140 139 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ↔ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ( -∞ (,) 𝑦 ) ) )
141 44 eleq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ↔ 𝐵 ∈ ( -∞ (,) 𝑦 ) ) )
142 141 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ↔ 𝐵 ∈ ( -∞ (,) 𝑦 ) ) )
143 138 140 142 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ) )
144 143 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) → ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
145 elpreima ⊢ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) Fn 𝐴 → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
146 102 103 145 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
147 146 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
148 elpreima ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
149 4 54 148 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
150 149 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
151 144 147 150 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( -∞ (,) 𝑦 ) ) ↔ 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ) )
152 151 alrimiv ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) → ∀ 𝑥 ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( -∞ (,) 𝑦 ) ) ↔ 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ) )
153 nfcv ⊢ Ⅎ 𝑥 ( -∞ (,) 𝑦 )
154 111 153 nfima ⊢ Ⅎ 𝑥 ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( -∞ (,) 𝑦 ) )
155 65 153 nfima ⊢ Ⅎ 𝑥 ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) )
156 154 155 cleqf ⊢ ( ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( -∞ (,) 𝑦 ) ) = ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( -∞ (,) 𝑦 ) ) ↔ 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ) )
157 152 156 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( -∞ (,) 𝑦 ) ) = ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) )
158 mbfima ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) : 𝐴 ⟶ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
159 2 102 158 syl2anc ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
160 159 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
161 157 160 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 0 < 𝑦 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
162 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ≤ 0 )
163 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
164 163 le0neg1d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ≤ 0 ↔ 0 ≤ - 𝑦 ) )
165 162 164 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ - 𝑦 )
166 165 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 ≤ - 𝑦 ↔ ( 0 ≤ - 𝑦 ∧ - 𝐵 ≤ - 𝑦 ) ) )
167 1 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
168 163 167 lenegd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ≤ 𝐵 ↔ - 𝐵 ≤ - 𝑦 ) )
169 0red ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ ℝ )
170 167 renegcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
171 163 renegcld ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → - 𝑦 ∈ ℝ )
172 maxle ⊢ ( ( 0 ∈ ℝ ∧ - 𝐵 ∈ ℝ ∧ - 𝑦 ∈ ℝ ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ≤ - 𝑦 ↔ ( 0 ≤ - 𝑦 ∧ - 𝐵 ≤ - 𝑦 ) ) )
173 169 170 171 172 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ≤ - 𝑦 ↔ ( 0 ≤ - 𝑦 ∧ - 𝐵 ≤ - 𝑦 ) ) )
174 166 168 173 3bitr4rd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ≤ - 𝑦 ↔ 𝑦 ≤ 𝐵 ) )
175 174 notbid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ≤ - 𝑦 ↔ ¬ 𝑦 ≤ 𝐵 ) )
176 24 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ )
177 171 176 ltnled ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( - 𝑦 < if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ↔ ¬ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ≤ - 𝑦 ) )
178 167 163 ltnled ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 < 𝑦 ↔ ¬ 𝑦 ≤ 𝐵 ) )
179 175 177 178 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( - 𝑦 < if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ↔ 𝐵 < 𝑦 ) )
180 176 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( - 𝑦 < if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ↔ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ ∧ - 𝑦 < if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
181 167 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 < 𝑦 ↔ ( 𝐵 ∈ ℝ ∧ 𝐵 < 𝑦 ) ) )
182 179 180 181 3bitr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ ∧ - 𝑦 < if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐵 < 𝑦 ) ) )
183 171 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → - 𝑦 ∈ ℝ* )
184 elioopnf ⊢ ( - 𝑦 ∈ ℝ* → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ( - 𝑦 (,) +∞ ) ↔ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ ∧ - 𝑦 < if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
185 183 184 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ( - 𝑦 (,) +∞ ) ↔ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ ∧ - 𝑦 < if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
186 163 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ* )
187 186 136 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ∈ ( -∞ (,) 𝑦 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐵 < 𝑦 ) ) )
188 182 185 187 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ( - 𝑦 (,) +∞ ) ↔ 𝐵 ∈ ( -∞ (,) 𝑦 ) ) )
189 39 eleq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( - 𝑦 (,) +∞ ) ↔ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ( - 𝑦 (,) +∞ ) ) )
190 189 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( - 𝑦 (,) +∞ ) ↔ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ( - 𝑦 (,) +∞ ) ) )
191 141 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ↔ 𝐵 ∈ ( -∞ (,) 𝑦 ) ) )
192 188 190 191 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( - 𝑦 (,) +∞ ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ) )
193 192 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) → ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( - 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
194 elpreima ⊢ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) Fn 𝐴 → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( - 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( - 𝑦 (,) +∞ ) ) ) )
195 49 50 194 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( - 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( - 𝑦 (,) +∞ ) ) ) )
196 195 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( - 𝑦 (,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ‘ 𝑥 ) ∈ ( - 𝑦 (,) +∞ ) ) ) )
197 149 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
198 193 196 197 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) → ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( - 𝑦 (,) +∞ ) ) ↔ 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ) )
199 198 alrimiv ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) → ∀ 𝑥 ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( - 𝑦 (,) +∞ ) ) ↔ 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ) )
200 nfcv ⊢ Ⅎ 𝑥 ( - 𝑦 (,) +∞ )
201 61 200 nfima ⊢ Ⅎ 𝑥 ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( - 𝑦 (,) +∞ ) )
202 201 155 cleqf ⊢ ( ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( - 𝑦 (,) +∞ ) ) = ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( - 𝑦 (,) +∞ ) ) ↔ 𝑥 ∈ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ) )
203 199 202 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( - 𝑦 (,) +∞ ) ) = ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) )
204 mbfima ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) : 𝐴 ⟶ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( - 𝑦 (,) +∞ ) ) ∈ dom vol )
205 3 49 204 syl2anc ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( - 𝑦 (,) +∞ ) ) ∈ dom vol )
206 205 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) “ ( - 𝑦 (,) +∞ ) ) ∈ dom vol )
207 203 206 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑦 ≤ 0 ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
208 161 207 120 119 ltlecasei ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
209 4 8 121 208 ismbf2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )