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 addlidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 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 eqtrid ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ ( 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 bitrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ∈ ( -∞ (,) 0 ) ↔ ¬ 0 ≤ 𝐵 ) )
182 181 rabbidva ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( -∞ (,) 0 ) } = { 𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵 } )
183 174 182 eqtrid ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) “ ( -∞ (,) 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 addridd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 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 bitrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 ∈ ( -∞ (,) 0 ) ↔ ¬ 0 ≤ 𝐶 ) )
252 251 rabbidva ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 ∈ ( -∞ (,) 0 ) } = { 𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶 } )
253 244 252 eqtrid ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) “ ( -∞ (,) 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 )