Metamath Proof Explorer


Theorem mbfposadd

Description: If the sum of two measurable functions is measurable, the sum of their nonnegative parts is measurable. (Contributed by Brendan Leahy, 2-Apr-2018)

Ref Expression
Hypotheses mbfposadd.1 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ MblFn )
mbfposadd.2 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
mbfposadd.3 ( 𝜑 → ( 𝑥𝐴𝐶 ) ∈ MblFn )
mbfposadd.4 ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ℝ )
mbfposadd.5 ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn )
Assertion mbfposadd ( 𝜑 → ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfposadd.1 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ MblFn )
2 mbfposadd.2 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
3 mbfposadd.3 ( 𝜑 → ( 𝑥𝐴𝐶 ) ∈ MblFn )
4 mbfposadd.4 ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ℝ )
5 mbfposadd.5 ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn )
6 0re 0 ∈ ℝ
7 ifcl ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
8 2 6 7 sylancl ( ( 𝜑𝑥𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
9 ifcl ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
10 4 6 9 sylancl ( ( 𝜑𝑥𝐴 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
11 8 10 readdcld ( ( 𝜑𝑥𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ℝ )
12 11 fmpttd ( 𝜑 → ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) : 𝐴 ⟶ ℝ )
13 ssrab2 { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ⊆ 𝐴
14 fssres ( ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) : 𝐴 ⟶ ℝ ∧ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ⊆ 𝐴 ) → ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) : { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ⟶ ℝ )
15 12 13 14 sylancl ( 𝜑 → ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) : { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ⟶ ℝ )
16 inss2 ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ { 𝑥𝐴 ∣ 0 ≤ 𝐶 }
17 resabs1 ( ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } → ( ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) )
18 16 17 ax-mp ( ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) )
19 elin ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↔ ( 𝑥 ∈ { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∧ 𝑥 ∈ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) )
20 rabid ( 𝑥 ∈ { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ↔ ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) )
21 rabid ( 𝑥 ∈ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ↔ ( 𝑥𝐴 ∧ 0 ≤ 𝐶 ) )
22 20 21 anbi12i ( ( 𝑥 ∈ { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∧ 𝑥 ∈ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↔ ( ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) ∧ ( 𝑥𝐴 ∧ 0 ≤ 𝐶 ) ) )
23 19 22 bitri ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↔ ( ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) ∧ ( 𝑥𝐴 ∧ 0 ≤ 𝐶 ) ) )
24 iftrue ( 0 ≤ 𝐵 → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) = 𝐵 )
25 iftrue ( 0 ≤ 𝐶 → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) = 𝐶 )
26 24 25 oveqan12d ( ( 0 ≤ 𝐵 ∧ 0 ≤ 𝐶 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = ( 𝐵 + 𝐶 ) )
27 26 ad2ant2l ( ( ( 𝑥𝐴 ∧ 0 ≤ 𝐵 ) ∧ ( 𝑥𝐴 ∧ 0 ≤ 𝐶 ) ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = ( 𝐵 + 𝐶 ) )
28 23 27 sylbi ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = ( 𝐵 + 𝐶 ) )
29 28 mpteq2ia ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( 𝐵 + 𝐶 ) )
30 inss1 ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ { 𝑥𝐴 ∣ 0 ≤ 𝐵 }
31 ssrab2 { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ⊆ 𝐴
32 30 31 sstri ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ 𝐴
33 resmpt ( ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ 𝐴 → ( ( 𝑦𝐴 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
34 nfcv 𝑦 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
35 nfcsb1v 𝑥 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
36 csbeq1a ( 𝑥 = 𝑦 → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
37 34 35 36 cbvmpt ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( 𝑦𝐴 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
38 37 reseq1i ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( ( 𝑦𝐴 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) )
39 nfv 𝑦 ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
40 nfrab1 𝑥 { 𝑥𝐴 ∣ 0 ≤ 𝐵 }
41 nfrab1 𝑥 { 𝑥𝐴 ∣ 0 ≤ 𝐶 }
42 40 41 nfin 𝑥 ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } )
43 42 nfcri 𝑥 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } )
44 35 nfeq2 𝑥 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
45 43 44 nfan 𝑥 ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
46 eleq1w ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↔ 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) )
47 36 eqeq2d ( 𝑥 = 𝑦 → ( 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ↔ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
48 46 47 anbi12d ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↔ ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ) )
49 39 45 48 cbvopab1 { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) }
50 df-mpt ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) }
51 df-mpt ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) }
52 49 50 51 3eqtr4i ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
53 33 38 52 3eqtr4g ( ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ 𝐴 → ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
54 32 53 ax-mp ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
55 resmpt ( ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ 𝐴 → ( ( 𝑦𝐴 𝑦 / 𝑥 ( 𝐵 + 𝐶 ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝑦 / 𝑥 ( 𝐵 + 𝐶 ) ) )
56 nfcv 𝑦 ( 𝐵 + 𝐶 )
57 nfcsb1v 𝑥 𝑦 / 𝑥 ( 𝐵 + 𝐶 )
58 csbeq1a ( 𝑥 = 𝑦 → ( 𝐵 + 𝐶 ) = 𝑦 / 𝑥 ( 𝐵 + 𝐶 ) )
59 56 57 58 cbvmpt ( 𝑥𝐴 ↦ ( 𝐵 + 𝐶 ) ) = ( 𝑦𝐴 𝑦 / 𝑥 ( 𝐵 + 𝐶 ) )
60 59 reseq1i ( ( 𝑥𝐴 ↦ ( 𝐵 + 𝐶 ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( ( 𝑦𝐴 𝑦 / 𝑥 ( 𝐵 + 𝐶 ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) )
61 nfv 𝑦 ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = ( 𝐵 + 𝐶 ) )
62 57 nfeq2 𝑥 𝑧 = 𝑦 / 𝑥 ( 𝐵 + 𝐶 )
63 43 62 nfan 𝑥 ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 ( 𝐵 + 𝐶 ) )
64 58 eqeq2d ( 𝑥 = 𝑦 → ( 𝑧 = ( 𝐵 + 𝐶 ) ↔ 𝑧 = 𝑦 / 𝑥 ( 𝐵 + 𝐶 ) ) )
65 46 64 anbi12d ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = ( 𝐵 + 𝐶 ) ) ↔ ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 ( 𝐵 + 𝐶 ) ) ) )
66 61 63 65 cbvopab1 { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = ( 𝐵 + 𝐶 ) ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 ( 𝐵 + 𝐶 ) ) }
67 df-mpt ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( 𝐵 + 𝐶 ) ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = ( 𝐵 + 𝐶 ) ) }
68 df-mpt ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝑦 / 𝑥 ( 𝐵 + 𝐶 ) ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 ( 𝐵 + 𝐶 ) ) }
69 66 67 68 3eqtr4i ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( 𝐵 + 𝐶 ) ) = ( 𝑦 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝑦 / 𝑥 ( 𝐵 + 𝐶 ) )
70 55 60 69 3eqtr4g ( ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ 𝐴 → ( ( 𝑥𝐴 ↦ ( 𝐵 + 𝐶 ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( 𝐵 + 𝐶 ) ) )
71 32 70 ax-mp ( ( 𝑥𝐴 ↦ ( 𝐵 + 𝐶 ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( 𝑥 ∈ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( 𝐵 + 𝐶 ) )
72 29 54 71 3eqtr4i ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( ( 𝑥𝐴 ↦ ( 𝐵 + 𝐶 ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) )
73 18 72 eqtri ( ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( ( 𝑥𝐴 ↦ ( 𝐵 + 𝐶 ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) )
74 2 biantrurd ( ( 𝜑𝑥𝐴 ) → ( 0 ≤ 𝐵 ↔ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) )
75 elrege0 ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
76 74 75 bitr4di ( ( 𝜑𝑥𝐴 ) → ( 0 ≤ 𝐵𝐵 ∈ ( 0 [,) +∞ ) ) )
77 76 rabbidva ( 𝜑 → { 𝑥𝐴 ∣ 0 ≤ 𝐵 } = { 𝑥𝐴𝐵 ∈ ( 0 [,) +∞ ) } )
78 0xr 0 ∈ ℝ*
79 pnfxr +∞ ∈ ℝ*
80 0ltpnf 0 < +∞
81 snunioo ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞ ) → ( { 0 } ∪ ( 0 (,) +∞ ) ) = ( 0 [,) +∞ ) )
82 78 79 80 81 mp3an ( { 0 } ∪ ( 0 (,) +∞ ) ) = ( 0 [,) +∞ )
83 82 imaeq2i ( ( 𝑥𝐴𝐵 ) “ ( { 0 } ∪ ( 0 (,) +∞ ) ) ) = ( ( 𝑥𝐴𝐵 ) “ ( 0 [,) +∞ ) )
84 imaundi ( ( 𝑥𝐴𝐵 ) “ ( { 0 } ∪ ( 0 (,) +∞ ) ) ) = ( ( ( 𝑥𝐴𝐵 ) “ { 0 } ) ∪ ( ( 𝑥𝐴𝐵 ) “ ( 0 (,) +∞ ) ) )
85 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
86 85 mptpreima ( ( 𝑥𝐴𝐵 ) “ ( 0 [,) +∞ ) ) = { 𝑥𝐴𝐵 ∈ ( 0 [,) +∞ ) }
87 83 84 86 3eqtr3ri { 𝑥𝐴𝐵 ∈ ( 0 [,) +∞ ) } = ( ( ( 𝑥𝐴𝐵 ) “ { 0 } ) ∪ ( ( 𝑥𝐴𝐵 ) “ ( 0 (,) +∞ ) ) )
88 77 87 eqtrdi ( 𝜑 → { 𝑥𝐴 ∣ 0 ≤ 𝐵 } = ( ( ( 𝑥𝐴𝐵 ) “ { 0 } ) ∪ ( ( 𝑥𝐴𝐵 ) “ ( 0 (,) +∞ ) ) ) )
89 2 fmpttd ( 𝜑 → ( 𝑥𝐴𝐵 ) : 𝐴 ⟶ ℝ )
90 mbfimasn ( ( ( 𝑥𝐴𝐵 ) ∈ MblFn ∧ ( 𝑥𝐴𝐵 ) : 𝐴 ⟶ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝑥𝐴𝐵 ) “ { 0 } ) ∈ dom vol )
91 6 90 mp3an3 ( ( ( 𝑥𝐴𝐵 ) ∈ MblFn ∧ ( 𝑥𝐴𝐵 ) : 𝐴 ⟶ ℝ ) → ( ( 𝑥𝐴𝐵 ) “ { 0 } ) ∈ dom vol )
92 mbfima ( ( ( 𝑥𝐴𝐵 ) ∈ MblFn ∧ ( 𝑥𝐴𝐵 ) : 𝐴 ⟶ ℝ ) → ( ( 𝑥𝐴𝐵 ) “ ( 0 (,) +∞ ) ) ∈ dom vol )
93 unmbl ( ( ( ( 𝑥𝐴𝐵 ) “ { 0 } ) ∈ dom vol ∧ ( ( 𝑥𝐴𝐵 ) “ ( 0 (,) +∞ ) ) ∈ dom vol ) → ( ( ( 𝑥𝐴𝐵 ) “ { 0 } ) ∪ ( ( 𝑥𝐴𝐵 ) “ ( 0 (,) +∞ ) ) ) ∈ dom vol )
94 91 92 93 syl2anc ( ( ( 𝑥𝐴𝐵 ) ∈ MblFn ∧ ( 𝑥𝐴𝐵 ) : 𝐴 ⟶ ℝ ) → ( ( ( 𝑥𝐴𝐵 ) “ { 0 } ) ∪ ( ( 𝑥𝐴𝐵 ) “ ( 0 (,) +∞ ) ) ) ∈ dom vol )
95 1 89 94 syl2anc ( 𝜑 → ( ( ( 𝑥𝐴𝐵 ) “ { 0 } ) ∪ ( ( 𝑥𝐴𝐵 ) “ ( 0 (,) +∞ ) ) ) ∈ dom vol )
96 88 95 eqeltrd ( 𝜑 → { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∈ dom vol )
97 4 biantrurd ( ( 𝜑𝑥𝐴 ) → ( 0 ≤ 𝐶 ↔ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) )
98 elrege0 ( 𝐶 ∈ ( 0 [,) +∞ ) ↔ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
99 97 98 bitr4di ( ( 𝜑𝑥𝐴 ) → ( 0 ≤ 𝐶𝐶 ∈ ( 0 [,) +∞ ) ) )
100 99 rabbidva ( 𝜑 → { 𝑥𝐴 ∣ 0 ≤ 𝐶 } = { 𝑥𝐴𝐶 ∈ ( 0 [,) +∞ ) } )
101 82 imaeq2i ( ( 𝑥𝐴𝐶 ) “ ( { 0 } ∪ ( 0 (,) +∞ ) ) ) = ( ( 𝑥𝐴𝐶 ) “ ( 0 [,) +∞ ) )
102 imaundi ( ( 𝑥𝐴𝐶 ) “ ( { 0 } ∪ ( 0 (,) +∞ ) ) ) = ( ( ( 𝑥𝐴𝐶 ) “ { 0 } ) ∪ ( ( 𝑥𝐴𝐶 ) “ ( 0 (,) +∞ ) ) )
103 eqid ( 𝑥𝐴𝐶 ) = ( 𝑥𝐴𝐶 )
104 103 mptpreima ( ( 𝑥𝐴𝐶 ) “ ( 0 [,) +∞ ) ) = { 𝑥𝐴𝐶 ∈ ( 0 [,) +∞ ) }
105 101 102 104 3eqtr3ri { 𝑥𝐴𝐶 ∈ ( 0 [,) +∞ ) } = ( ( ( 𝑥𝐴𝐶 ) “ { 0 } ) ∪ ( ( 𝑥𝐴𝐶 ) “ ( 0 (,) +∞ ) ) )
106 100 105 eqtrdi ( 𝜑 → { 𝑥𝐴 ∣ 0 ≤ 𝐶 } = ( ( ( 𝑥𝐴𝐶 ) “ { 0 } ) ∪ ( ( 𝑥𝐴𝐶 ) “ ( 0 (,) +∞ ) ) ) )
107 4 fmpttd ( 𝜑 → ( 𝑥𝐴𝐶 ) : 𝐴 ⟶ ℝ )
108 mbfimasn ( ( ( 𝑥𝐴𝐶 ) ∈ MblFn ∧ ( 𝑥𝐴𝐶 ) : 𝐴 ⟶ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝑥𝐴𝐶 ) “ { 0 } ) ∈ dom vol )
109 6 108 mp3an3 ( ( ( 𝑥𝐴𝐶 ) ∈ MblFn ∧ ( 𝑥𝐴𝐶 ) : 𝐴 ⟶ ℝ ) → ( ( 𝑥𝐴𝐶 ) “ { 0 } ) ∈ dom vol )
110 mbfima ( ( ( 𝑥𝐴𝐶 ) ∈ MblFn ∧ ( 𝑥𝐴𝐶 ) : 𝐴 ⟶ ℝ ) → ( ( 𝑥𝐴𝐶 ) “ ( 0 (,) +∞ ) ) ∈ dom vol )
111 unmbl ( ( ( ( 𝑥𝐴𝐶 ) “ { 0 } ) ∈ dom vol ∧ ( ( 𝑥𝐴𝐶 ) “ ( 0 (,) +∞ ) ) ∈ dom vol ) → ( ( ( 𝑥𝐴𝐶 ) “ { 0 } ) ∪ ( ( 𝑥𝐴𝐶 ) “ ( 0 (,) +∞ ) ) ) ∈ dom vol )
112 109 110 111 syl2anc ( ( ( 𝑥𝐴𝐶 ) ∈ MblFn ∧ ( 𝑥𝐴𝐶 ) : 𝐴 ⟶ ℝ ) → ( ( ( 𝑥𝐴𝐶 ) “ { 0 } ) ∪ ( ( 𝑥𝐴𝐶 ) “ ( 0 (,) +∞ ) ) ) ∈ dom vol )
113 3 107 112 syl2anc ( 𝜑 → ( ( ( 𝑥𝐴𝐶 ) “ { 0 } ) ∪ ( ( 𝑥𝐴𝐶 ) “ ( 0 (,) +∞ ) ) ) ∈ dom vol )
114 106 113 eqeltrd ( 𝜑 → { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ∈ dom vol )
115 inmbl ( ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∈ dom vol ∧ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ∈ dom vol ) → ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∈ dom vol )
116 96 114 115 syl2anc ( 𝜑 → ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∈ dom vol )
117 mbfres ( ( ( 𝑥𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn ∧ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∈ dom vol ) → ( ( 𝑥𝐴 ↦ ( 𝐵 + 𝐶 ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) ∈ MblFn )
118 5 116 117 syl2anc ( 𝜑 → ( ( 𝑥𝐴 ↦ ( 𝐵 + 𝐶 ) ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) ∈ MblFn )
119 73 118 eqeltrid ( 𝜑 → ( ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↾ ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) ∈ MblFn )
120 inss2 ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ { 𝑥𝐴 ∣ 0 ≤ 𝐶 }
121 resabs1 ( ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } → ( ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) )
122 120 121 ax-mp ( ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) )
123 rabid ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ↔ ( 𝑥𝐴 ∧ ¬ 0 ≤ 𝐵 ) )
124 123 21 anbi12i ( ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∧ 𝑥 ∈ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↔ ( ( 𝑥𝐴 ∧ ¬ 0 ≤ 𝐵 ) ∧ ( 𝑥𝐴 ∧ 0 ≤ 𝐶 ) ) )
125 elin ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↔ ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∧ 𝑥 ∈ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) )
126 anandi ( ( 𝑥𝐴 ∧ ( ¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶 ) ) ↔ ( ( 𝑥𝐴 ∧ ¬ 0 ≤ 𝐵 ) ∧ ( 𝑥𝐴 ∧ 0 ≤ 𝐶 ) ) )
127 124 125 126 3bitr4i ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↔ ( 𝑥𝐴 ∧ ( ¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶 ) ) )
128 iffalse ( ¬ 0 ≤ 𝐵 → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) = 0 )
129 128 25 oveqan12d ( ( ¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = ( 0 + 𝐶 ) )
130 129 ad2antll ( ( 𝜑 ∧ ( 𝑥𝐴 ∧ ( ¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶 ) ) ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = ( 0 + 𝐶 ) )
131 4 recnd ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ℂ )
132 131 addid2d ( ( 𝜑𝑥𝐴 ) → ( 0 + 𝐶 ) = 𝐶 )
133 132 adantrr ( ( 𝜑 ∧ ( 𝑥𝐴 ∧ ( ¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶 ) ) ) → ( 0 + 𝐶 ) = 𝐶 )
134 130 133 eqtrd ( ( 𝜑 ∧ ( 𝑥𝐴 ∧ ( ¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶 ) ) ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = 𝐶 )
135 127 134 sylan2b ( ( 𝜑𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = 𝐶 )
136 135 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝐶 ) )
137 inss1 ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 }
138 ssrab2 { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ⊆ 𝐴
139 137 138 sstri ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ 𝐴
140 resmpt ( ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ 𝐴 → ( ( 𝑦𝐴 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
141 37 reseq1i ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( ( 𝑦𝐴 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) )
142 nfv 𝑦 ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
143 nfrab1 𝑥 { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 }
144 143 41 nfin 𝑥 ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } )
145 144 nfcri 𝑥 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } )
146 145 44 nfan 𝑥 ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
147 eleq1w ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↔ 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) )
148 147 47 anbi12d ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↔ ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ) )
149 142 146 148 cbvopab1 { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) }
150 df-mpt ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) }
151 df-mpt ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) }
152 149 150 151 3eqtr4i ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
153 140 141 152 3eqtr4g ( ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ 𝐴 → ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
154 139 153 ax-mp ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
155 resmpt ( ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ 𝐴 → ( ( 𝑦𝐴 𝑦 / 𝑥 𝐶 ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝑦 / 𝑥 𝐶 ) )
156 nfcv 𝑦 𝐶
157 nfcsb1v 𝑥 𝑦 / 𝑥 𝐶
158 csbeq1a ( 𝑥 = 𝑦𝐶 = 𝑦 / 𝑥 𝐶 )
159 156 157 158 cbvmpt ( 𝑥𝐴𝐶 ) = ( 𝑦𝐴 𝑦 / 𝑥 𝐶 )
160 159 reseq1i ( ( 𝑥𝐴𝐶 ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( ( 𝑦𝐴 𝑦 / 𝑥 𝐶 ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) )
161 nfv 𝑦 ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝐶 )
162 157 nfeq2 𝑥 𝑧 = 𝑦 / 𝑥 𝐶
163 145 162 nfan 𝑥 ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 𝐶 )
164 158 eqeq2d ( 𝑥 = 𝑦 → ( 𝑧 = 𝐶𝑧 = 𝑦 / 𝑥 𝐶 ) )
165 147 164 anbi12d ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝐶 ) ↔ ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 𝐶 ) ) )
166 161 163 165 cbvopab1 { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝐶 ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 𝐶 ) }
167 df-mpt ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝐶 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝐶 ) }
168 df-mpt ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝑦 / 𝑥 𝐶 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∧ 𝑧 = 𝑦 / 𝑥 𝐶 ) }
169 166 167 168 3eqtr4i ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝐶 ) = ( 𝑦 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝑦 / 𝑥 𝐶 )
170 155 160 169 3eqtr4g ( ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ⊆ 𝐴 → ( ( 𝑥𝐴𝐶 ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝐶 ) )
171 139 170 ax-mp ( ( 𝑥𝐴𝐶 ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( 𝑥 ∈ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↦ 𝐶 )
172 136 154 171 3eqtr4g ( 𝜑 → ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( ( 𝑥𝐴𝐶 ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) )
173 122 172 syl5eq ( 𝜑 → ( ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = ( ( 𝑥𝐴𝐶 ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) )
174 85 mptpreima ( ( 𝑥𝐴𝐵 ) “ ( -∞ (,) 0 ) ) = { 𝑥𝐴𝐵 ∈ ( -∞ (,) 0 ) }
175 elioomnf ( 0 ∈ ℝ* → ( 𝐵 ∈ ( -∞ (,) 0 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐵 < 0 ) ) )
176 78 175 ax-mp ( 𝐵 ∈ ( -∞ (,) 0 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐵 < 0 ) )
177 2 biantrurd ( ( 𝜑𝑥𝐴 ) → ( 𝐵 < 0 ↔ ( 𝐵 ∈ ℝ ∧ 𝐵 < 0 ) ) )
178 ltnle ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐵 < 0 ↔ ¬ 0 ≤ 𝐵 ) )
179 2 6 178 sylancl ( ( 𝜑𝑥𝐴 ) → ( 𝐵 < 0 ↔ ¬ 0 ≤ 𝐵 ) )
180 177 179 bitr3d ( ( 𝜑𝑥𝐴 ) → ( ( 𝐵 ∈ ℝ ∧ 𝐵 < 0 ) ↔ ¬ 0 ≤ 𝐵 ) )
181 176 180 syl5bb ( ( 𝜑𝑥𝐴 ) → ( 𝐵 ∈ ( -∞ (,) 0 ) ↔ ¬ 0 ≤ 𝐵 ) )
182 181 rabbidva ( 𝜑 → { 𝑥𝐴𝐵 ∈ ( -∞ (,) 0 ) } = { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } )
183 174 182 syl5eq ( 𝜑 → ( ( 𝑥𝐴𝐵 ) “ ( -∞ (,) 0 ) ) = { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } )
184 mbfima ( ( ( 𝑥𝐴𝐵 ) ∈ MblFn ∧ ( 𝑥𝐴𝐵 ) : 𝐴 ⟶ ℝ ) → ( ( 𝑥𝐴𝐵 ) “ ( -∞ (,) 0 ) ) ∈ dom vol )
185 1 89 184 syl2anc ( 𝜑 → ( ( 𝑥𝐴𝐵 ) “ ( -∞ (,) 0 ) ) ∈ dom vol )
186 183 185 eqeltrrd ( 𝜑 → { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∈ dom vol )
187 inmbl ( ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∈ dom vol ∧ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ∈ dom vol ) → ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∈ dom vol )
188 186 114 187 syl2anc ( 𝜑 → ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∈ dom vol )
189 mbfres ( ( ( 𝑥𝐴𝐶 ) ∈ MblFn ∧ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∈ dom vol ) → ( ( 𝑥𝐴𝐶 ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) ∈ MblFn )
190 3 188 189 syl2anc ( 𝜑 → ( ( 𝑥𝐴𝐶 ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) ∈ MblFn )
191 173 190 eqeltrd ( 𝜑 → ( ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ↾ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) ∈ MblFn )
192 ssid 𝐴𝐴
193 dfrab3ss ( 𝐴𝐴 → { 𝑥𝐴 ∣ 0 ≤ 𝐶 } = ( 𝐴 ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) )
194 192 193 ax-mp { 𝑥𝐴 ∣ 0 ≤ 𝐶 } = ( 𝐴 ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } )
195 rabxm 𝐴 = ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∪ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } )
196 195 ineq1i ( 𝐴 ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) = ( ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∪ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ) ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } )
197 indir ( ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∪ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ) ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) = ( ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∪ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) )
198 194 196 197 3eqtrri ( ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∪ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = { 𝑥𝐴 ∣ 0 ≤ 𝐶 }
199 198 a1i ( 𝜑 → ( ( { 𝑥𝐴 ∣ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∪ ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐵 } ∩ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ) = { 𝑥𝐴 ∣ 0 ≤ 𝐶 } )
200 15 119 191 199 mbfres2 ( 𝜑 → ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ) ∈ MblFn )
201 rabid ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↔ ( 𝑥𝐴 ∧ ¬ 0 ≤ 𝐶 ) )
202 iffalse ( ¬ 0 ≤ 𝐶 → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) = 0 )
203 202 oveq2d ( ¬ 0 ≤ 𝐶 → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + 0 ) )
204 8 recnd ( ( 𝜑𝑥𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℂ )
205 204 addid1d ( ( 𝜑𝑥𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + 0 ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
206 203 205 sylan9eqr ( ( ( 𝜑𝑥𝐴 ) ∧ ¬ 0 ≤ 𝐶 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
207 206 anasss ( ( 𝜑 ∧ ( 𝑥𝐴 ∧ ¬ 0 ≤ 𝐶 ) ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
208 201 207 sylan2b ( ( 𝜑𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
209 208 mpteq2dva ( 𝜑 → ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) )
210 ssrab2 { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ⊆ 𝐴
211 resmpt ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ⊆ 𝐴 → ( ( 𝑦𝐴 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) = ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
212 37 reseq1i ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) = ( ( 𝑦𝐴 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } )
213 nfv 𝑦 ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
214 nfrab1 𝑥 { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 }
215 214 nfcri 𝑥 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 }
216 215 44 nfan 𝑥 ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
217 eleq1w ( 𝑥 = 𝑦 → ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↔ 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) )
218 217 47 anbi12d ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↔ ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ) )
219 213 216 218 cbvopab1 { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) }
220 df-mpt ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) }
221 df-mpt ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) }
222 219 220 221 3eqtr4i ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ 𝑦 / 𝑥 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
223 211 212 222 3eqtr4g ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ⊆ 𝐴 → ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) = ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
224 210 223 ax-mp ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) = ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
225 resmpt ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ⊆ 𝐴 → ( ( 𝑦𝐴 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) = ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) )
226 nfcv 𝑦 if ( 0 ≤ 𝐵 , 𝐵 , 0 )
227 nfcsb1v 𝑥 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 )
228 csbeq1a ( 𝑥 = 𝑦 → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) = 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
229 226 227 228 cbvmpt ( 𝑥𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = ( 𝑦𝐴 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
230 229 reseq1i ( ( 𝑥𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) = ( ( 𝑦𝐴 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } )
231 nfv 𝑦 ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
232 227 nfeq2 𝑥 𝑧 = 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 )
233 215 232 nfan 𝑥 ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
234 228 eqeq2d ( 𝑥 = 𝑦 → ( 𝑧 = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ↔ 𝑧 = 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) )
235 217 234 anbi12d ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ↔ ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) )
236 231 233 235 cbvopab1 { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) }
237 df-mpt ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) }
238 df-mpt ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∧ 𝑧 = 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) }
239 236 237 238 3eqtr4i ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = ( 𝑦 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ 𝑦 / 𝑥 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
240 225 230 239 3eqtr4g ( { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ⊆ 𝐴 → ( ( 𝑥𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) = ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) )
241 210 240 ax-mp ( ( 𝑥𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) = ( 𝑥 ∈ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
242 209 224 241 3eqtr4g ( 𝜑 → ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) = ( ( 𝑥𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) )
243 2 1 mbfpos ( 𝜑 → ( 𝑥𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn )
244 103 mptpreima ( ( 𝑥𝐴𝐶 ) “ ( -∞ (,) 0 ) ) = { 𝑥𝐴𝐶 ∈ ( -∞ (,) 0 ) }
245 elioomnf ( 0 ∈ ℝ* → ( 𝐶 ∈ ( -∞ (,) 0 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐶 < 0 ) ) )
246 78 245 ax-mp ( 𝐶 ∈ ( -∞ (,) 0 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐶 < 0 ) )
247 4 biantrurd ( ( 𝜑𝑥𝐴 ) → ( 𝐶 < 0 ↔ ( 𝐶 ∈ ℝ ∧ 𝐶 < 0 ) ) )
248 ltnle ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐶 < 0 ↔ ¬ 0 ≤ 𝐶 ) )
249 4 6 248 sylancl ( ( 𝜑𝑥𝐴 ) → ( 𝐶 < 0 ↔ ¬ 0 ≤ 𝐶 ) )
250 247 249 bitr3d ( ( 𝜑𝑥𝐴 ) → ( ( 𝐶 ∈ ℝ ∧ 𝐶 < 0 ) ↔ ¬ 0 ≤ 𝐶 ) )
251 246 250 syl5bb ( ( 𝜑𝑥𝐴 ) → ( 𝐶 ∈ ( -∞ (,) 0 ) ↔ ¬ 0 ≤ 𝐶 ) )
252 251 rabbidva ( 𝜑 → { 𝑥𝐴𝐶 ∈ ( -∞ (,) 0 ) } = { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } )
253 244 252 syl5eq ( 𝜑 → ( ( 𝑥𝐴𝐶 ) “ ( -∞ (,) 0 ) ) = { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } )
254 mbfima ( ( ( 𝑥𝐴𝐶 ) ∈ MblFn ∧ ( 𝑥𝐴𝐶 ) : 𝐴 ⟶ ℝ ) → ( ( 𝑥𝐴𝐶 ) “ ( -∞ (,) 0 ) ) ∈ dom vol )
255 3 107 254 syl2anc ( 𝜑 → ( ( 𝑥𝐴𝐶 ) “ ( -∞ (,) 0 ) ) ∈ dom vol )
256 253 255 eqeltrrd ( 𝜑 → { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∈ dom vol )
257 mbfres ( ( ( 𝑥𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ∈ dom vol ) → ( ( 𝑥𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) ∈ MblFn )
258 243 256 257 syl2anc ( 𝜑 → ( ( 𝑥𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) ∈ MblFn )
259 242 258 eqeltrd ( 𝜑 → ( ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ↾ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) ∈ MblFn )
260 rabxm 𝐴 = ( { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ∪ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } )
261 260 eqcomi ( { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ∪ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) = 𝐴
262 261 a1i ( 𝜑 → ( { 𝑥𝐴 ∣ 0 ≤ 𝐶 } ∪ { 𝑥𝐴 ∣ ¬ 0 ≤ 𝐶 } ) = 𝐴 )
263 12 200 259 262 mbfres2 ( 𝜑 → ( 𝑥𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ∈ MblFn )