Theorem mbfposadd 32627

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.)

Hypotheses

Ref	Expression
mbfposadd.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
mbfposadd.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
mbfposadd.3	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
mbfposadd.4	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)
mbfposadd.5	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)

Assertion

Ref	Expression
mbfposadd	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ MblFn)

Distinct variable groups:   𝜑,𝑥   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mbfposadd

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mbfposadd.2	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
2		0re 9919	. . . . 5 ⊢ 0 ∈ ℝ
3		ifcl 4080	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
4	1, 2, 3	sylancl 693	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
5		mbfposadd.4	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)
6		ifcl 4080	. . . . 5 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
7	5, 2, 6	sylancl 693	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
8	4, 7	readdcld 9948	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ)
9		eqid 2610	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
10	8, 9	fmptd 6292	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))):𝐴⟶ℝ)
11		ssrab2 3650	. . . 4 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ⊆ 𝐴
12		fssres 5983	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))):𝐴⟶ℝ ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ⊆ 𝐴) → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}):{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}⟶ℝ)
13	10, 11, 12	sylancl 693	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}):{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}⟶ℝ)
14		inss2 3796	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
15		resabs1 5347	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
16	14, 15	ax-mp 5	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
17		elin 3758	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
18		rabid 3095	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))
19		rabid 3095	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶))
20	18, 19	anbi12i 729	. . . . . . . . 9 ⊢ ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
21	17, 20	bitri 263	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
22		iftrue 4042	. . . . . . . . . 10 ⊢ (0 ≤ 𝐵 → if(0 ≤ 𝐵, 𝐵, 0) = 𝐵)
23		iftrue 4042	. . . . . . . . . 10 ⊢ (0 ≤ 𝐶 → if(0 ≤ 𝐶, 𝐶, 0) = 𝐶)
24	22, 23	oveqan12d 6568	. . . . . . . . 9 ⊢ ((0 ≤ 𝐵 ∧ 0 ≤ 𝐶) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (𝐵 + 𝐶))
25	24	ad2ant2l 778	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (𝐵 + 𝐶))
26	21, 25	sylbi 206	. . . . . . 7 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (𝐵 + 𝐶))
27	26	mpteq2ia 4668	. . . . . 6 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶))
28		inss1 3795	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵}
29		ssrab2 3650	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ⊆ 𝐴
30	28, 29	sstri 3577	. . . . . . 7 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴
31		resmpt 5369	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
32		nfcv 2751	. . . . . . . . . 10 ⊢ Ⅎ𝑦(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
33		nfcsb1v 3515	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
34		csbeq1a 3508	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
35	32, 33, 34	cbvmpt 4677	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
36	35	reseq1i 5313	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
37		nfv 1830	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
38		nfrab1 3099	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵}
39		nfrab1 3099	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
40	38, 39	nfin 3782	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
41	40	nfcri 2745	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
42	33	nfeq2 2766	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
43	41, 42	nfan 1816	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
44		eleq1 2676	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
45	34	eqeq2d 2620	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
46	44, 45	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))))
47	37, 43, 46	cbvopab1 4655	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
48		df-mpt 4645	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
49		df-mpt 4645	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
50	47, 48, 49	3eqtr4i 2642	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
51	31, 36, 50	3eqtr4g 2669	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
52	30, 51	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
53		resmpt 5369	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)))
54		nfcv 2751	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝐵 + 𝐶)
55		nfcsb1v 3515	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)
56		csbeq1a 3508	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝐵 + 𝐶) = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
57	54, 55, 56	cbvmpt 4677	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
58	57	reseq1i 5313	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
59		nfv 1830	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))
60	55	nfeq2 2766	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)
61	41, 60	nfan 1816	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
62	56	eqeq2d 2620	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = (𝐵 + 𝐶) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)))
63	44, 62	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶)) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))))
64	59, 61, 63	cbvopab1 4655	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))}
65		df-mpt 4645	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))}
66		df-mpt 4645	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))}
67	64, 65, 66	3eqtr4i 2642	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
68	53, 58, 67	3eqtr4g 2669	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)))
69	30, 68	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶))
70	27, 52, 69	3eqtr4i 2642	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
71	16, 70	eqtri 2632	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
72		mbfposadd.5	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)
73	1	biantrurd 528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)))
74		elrege0 12149	. . . . . . . . . 10 ⊢ (𝐵 ∈ (0[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵))
75	73, 74	syl6bbr 277	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ 𝐵 ∈ (0[,)+∞)))
76	75	rabbidva 3163	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)})
77		0xr 9965	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ*
78		pnfxr 9971	. . . . . . . . . . 11 ⊢ +∞ ∈ ℝ*
79		0ltpnf 11832	. . . . . . . . . . 11 ⊢ 0 < +∞
80		snunioo 12169	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) → ({0} ∪ (0(,)+∞)) = (0[,)+∞))
81	77, 78, 79, 80	mp3an 1416	. . . . . . . . . 10 ⊢ ({0} ∪ (0(,)+∞)) = (0[,)+∞)
82	81	imaeq2i 5383	. . . . . . . . 9 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ ({0} ∪ (0(,)+∞))) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0[,)+∞))
83		imaundi 5464	. . . . . . . . 9 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ ({0} ∪ (0(,)+∞))) = ((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)))
84		eqid 2610	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
85	84	mptpreima 5545	. . . . . . . . 9 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0[,)+∞)) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)}
86	82, 83, 85	3eqtr3ri 2641	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)} = ((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)))
87	76, 86	syl6eq 2660	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} = ((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))))
88		mbfposadd.1	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
89	1, 84	fmptd 6292	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ)
90		mbfimasn 23207	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ ∧ 0 ∈ ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol)
91	2, 90	mp3an3 1405	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol)
92		mbfima 23205	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)) ∈ dom vol)
93		unmbl 23112	. . . . . . . . 9 ⊢ (((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol ∧ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)) ∈ dom vol) → ((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))) ∈ dom vol)
94	91, 92, 93	syl2anc 691	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → ((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))) ∈ dom vol)
95	88, 89, 94	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → ((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))) ∈ dom vol)
96	87, 95	eqeltrd 2688	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∈ dom vol)
97	5	biantrurd 528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)))
98		elrege0 12149	. . . . . . . . . 10 ⊢ (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
99	97, 98	syl6bbr 277	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ 𝐶 ∈ (0[,)+∞)))
100	99	rabbidva 3163	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)})
101	81	imaeq2i 5383	. . . . . . . . 9 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ ({0} ∪ (0(,)+∞))) = (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0[,)+∞))
102		imaundi 5464	. . . . . . . . 9 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ ({0} ∪ (0(,)+∞))) = ((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)))
103		eqid 2610	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶)
104	103	mptpreima 5545	. . . . . . . . 9 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0[,)+∞)) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)}
105	101, 102, 104	3eqtr3ri 2641	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)} = ((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)))
106	100, 105	syl6eq 2660	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = ((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))))
107		mbfposadd.3	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
108	5, 103	fmptd 6292	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ)
109		mbfimasn 23207	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ ∧ 0 ∈ ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol)
110	2, 109	mp3an3 1405	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol)
111		mbfima 23205	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)) ∈ dom vol)
112		unmbl 23112	. . . . . . . . 9 ⊢ (((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol ∧ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)) ∈ dom vol) → ((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))) ∈ dom vol)
113	110, 111, 112	syl2anc 691	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → ((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))) ∈ dom vol)
114	107, 108, 113	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → ((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))) ∈ dom vol)
115	106, 114	eqeltrd 2688	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol)
116		inmbl 23117	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∈ dom vol ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol) → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
117	96, 115, 116	syl2anc 691	. . . . 5 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
118		mbfres 23217	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn ∧ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol) → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
119	72, 117, 118	syl2anc 691	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
120	71, 119	syl5eqel 2692	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
121		inss2 3796	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
122		resabs1 5347	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
123	121, 122	ax-mp 5	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
124		rabid 3095	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵))
125	124, 19	anbi12i 729	. . . . . . . . 9 ⊢ ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
126		elin 3758	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
127		anandi 867	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
128	125, 126, 127	3bitr4i 291	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶)))
129		iffalse 4045	. . . . . . . . . . 11 ⊢ (¬ 0 ≤ 𝐵 → if(0 ≤ 𝐵, 𝐵, 0) = 0)
130	129, 23	oveqan12d 6568	. . . . . . . . . 10 ⊢ ((¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (0 + 𝐶))
131	130	ad2antll 761	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶))) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (0 + 𝐶))
132	5	recnd 9947	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
133	132	addid2d 10116	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 + 𝐶) = 𝐶)
134	133	adantrr 749	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶))) → (0 + 𝐶) = 𝐶)
135	131, 134	eqtrd 2644	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶))) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = 𝐶)
136	128, 135	sylan2b 491	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = 𝐶)
137	136	mpteq2dva 4672	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶))
138		inss1 3795	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}
139		ssrab2 3650	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ⊆ 𝐴
140	138, 139	sstri 3577	. . . . . . 7 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴
141		resmpt 5369	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
142	35	reseq1i 5313	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
143		nfv 1830	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
144		nfrab1 3099	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}
145	144, 39	nfin 3782	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
146	145	nfcri 2745	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
147	146, 42	nfan 1816	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
148		eleq1 2676	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
149	148, 45	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))))
150	143, 147, 149	cbvopab1 4655	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
151		df-mpt 4645	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
152		df-mpt 4645	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
153	150, 151, 152	3eqtr4i 2642	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
154	141, 142, 153	3eqtr4g 2669	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
155	140, 154	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
156		resmpt 5369	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶))
157		nfcv 2751	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐶
158		nfcsb1v 3515	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶
159		csbeq1a 3508	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶)
160	157, 158, 159	cbvmpt 4677	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶)
161	160	reseq1i 5313	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
162		nfv 1830	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)
163	158	nfeq2 2766	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌𝐶
164	146, 163	nfan 1816	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)
165	159	eqeq2d 2620	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐶 ↔ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶))
166	148, 165	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)))
167	162, 164, 166	cbvopab1 4655	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)}
168		df-mpt 4645	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)}
169		df-mpt 4645	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)}
170	167, 168, 169	3eqtr4i 2642	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶)
171	156, 161, 170	3eqtr4g 2669	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶))
172	140, 171	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶)
173	137, 155, 172	3eqtr4g 2669	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
174	123, 173	syl5eq 2656	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
175	84	mptpreima 5545	. . . . . . . 8 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (-∞(,)0)}
176		elioomnf 12139	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ* → (𝐵 ∈ (-∞(,)0) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0)))
177	77, 176	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐵 ∈ (-∞(,)0) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0))
178	1	biantrurd 528	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 < 0 ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0)))
179		ltnle 9996	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
180	1, 2, 179	sylancl 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
181	178, 180	bitr3d 269	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ ℝ ∧ 𝐵 < 0) ↔ ¬ 0 ≤ 𝐵))
182	177, 181	syl5bb 271	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ (-∞(,)0) ↔ ¬ 0 ≤ 𝐵))
183	182	rabbidva 3163	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (-∞(,)0)} = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
184	175, 183	syl5eq 2656	. . . . . . 7 ⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
185		mbfima 23205	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) ∈ dom vol)
186	88, 89, 185	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) ∈ dom vol)
187	184, 186	eqeltrrd 2689	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∈ dom vol)
188		inmbl 23117	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∈ dom vol ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol) → ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
189	187, 115, 188	syl2anc 691	. . . . 5 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
190		mbfres 23217	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol) → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
191	107, 189, 190	syl2anc 691	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
192	174, 191	eqeltrd 2688	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
193		ssid 3587	. . . . . 6 ⊢ 𝐴 ⊆ 𝐴
194		dfrab3ss 3864	. . . . . 6 ⊢ (𝐴 ⊆ 𝐴 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
195	193, 194	ax-mp 5	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
196		rabxm 3915	. . . . . 6 ⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
197	196	ineq1i 3772	. . . . 5 ⊢ (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) = (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}) ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
198		indir 3834	. . . . 5 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}) ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) = (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
199	195, 197, 198	3eqtrri 2637	. . . 4 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
200	199	a1i 11	. . 3 ⊢ (𝜑 → (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
201	13, 120, 192, 200	mbfres2 23218	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ MblFn)
202		rabid 3095	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐶))
203		iffalse 4045	. . . . . . . . 9 ⊢ (¬ 0 ≤ 𝐶 → if(0 ≤ 𝐶, 𝐶, 0) = 0)
204	203	oveq2d 6565	. . . . . . . 8 ⊢ (¬ 0 ≤ 𝐶 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (if(0 ≤ 𝐵, 𝐵, 0) + 0))
205	4	recnd 9947	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℂ)
206	205	addid1d 10115	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + 0) = if(0 ≤ 𝐵, 𝐵, 0))
207	204, 206	sylan9eqr 2666	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 0 ≤ 𝐶) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
208	207	anasss 677	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐶)) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
209	202, 208	sylan2b 491	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
210	209	mpteq2dva 4672	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)))
211		ssrab2 3650	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴
212		resmpt 5369	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
213	35	reseq1i 5313	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
214		nfv 1830	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
215		nfrab1 3099	. . . . . . . . . 10 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}
216	215	nfcri 2745	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}
217	216, 42	nfan 1816	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
218		eleq1 2676	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↔ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}))
219	218, 45	anbi12d 743	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↔ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))))
220	214, 217, 219	cbvopab1 4655	. . . . . . 7 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
221		df-mpt 4645	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
222		df-mpt 4645	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
223	220, 221, 222	3eqtr4i 2642	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
224	212, 213, 223	3eqtr4g 2669	. . . . 5 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
225	211, 224	ax-mp 5	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
226		resmpt 5369	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)))
227		nfcv 2751	. . . . . . . 8 ⊢ Ⅎ𝑦if(0 ≤ 𝐵, 𝐵, 0)
228		nfcsb1v 3515	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)
229		csbeq1a 3508	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → if(0 ≤ 𝐵, 𝐵, 0) = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
230	227, 228, 229	cbvmpt 4677	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
231	230	reseq1i 5313	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
232		nfv 1830	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))
233	228	nfeq2 2766	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)
234	216, 233	nfan 1816	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
235	229	eqeq2d 2620	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑧 = if(0 ≤ 𝐵, 𝐵, 0) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)))
236	218, 235	anbi12d 743	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0)) ↔ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))))
237	232, 234, 236	cbvopab1 4655	. . . . . . 7 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))}
238		df-mpt 4645	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))}
239		df-mpt 4645	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))}
240	237, 238, 239	3eqtr4i 2642	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
241	226, 231, 240	3eqtr4g 2669	. . . . 5 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)))
242	211, 241	ax-mp 5	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0))
243	210, 225, 242	3eqtr4g 2669	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}))
244	1, 88	mbfpos 23224	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)
245	103	mptpreima 5545	. . . . . 6 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (-∞(,)0)}
246		elioomnf 12139	. . . . . . . . 9 ⊢ (0 ∈ ℝ* → (𝐶 ∈ (-∞(,)0) ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0)))
247	77, 246	ax-mp 5	. . . . . . . 8 ⊢ (𝐶 ∈ (-∞(,)0) ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0))
248	5	biantrurd 528	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 < 0 ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0)))
249		ltnle 9996	. . . . . . . . . 10 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
250	5, 2, 249	sylancl 693	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
251	248, 250	bitr3d 269	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐶 ∈ ℝ ∧ 𝐶 < 0) ↔ ¬ 0 ≤ 𝐶))
252	247, 251	syl5bb 271	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ∈ (-∞(,)0) ↔ ¬ 0 ≤ 𝐶))
253	252	rabbidva 3163	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (-∞(,)0)} = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
254	245, 253	syl5eq 2656	. . . . 5 ⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
255		mbfima 23205	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) ∈ dom vol)
256	107, 108, 255	syl2anc 691	. . . . 5 ⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) ∈ dom vol)
257	254, 256	eqeltrrd 2689	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∈ dom vol)
258		mbfres 23217	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∈ dom vol) → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) ∈ MblFn)
259	244, 257, 258	syl2anc 691	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) ∈ MblFn)
260	243, 259	eqeltrd 2688	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) ∈ MblFn)
261		rabxm 3915	. . . 4 ⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
262	261	eqcomi 2619	. . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = 𝐴
263	262	a1i 11	. 2 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = 𝐴)
264	10, 201, 260, 263	mbfres2 23218	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ MblFn)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {crab 2900  ⦋csb 3499   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ifcif 4036  {csn 4125   class class class wbr 4583  {copab 4642   ↦ cmpt 4643  ^◡ccnv 5037  dom cdm 5038   ↾ cres 5040   “ cima 5041  ⟶wf 5800  (class class class)co 6549  ℝcr 9814  0cc0 9815   + caddc 9818  +∞cpnf 9950  -∞cmnf 9951  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954  (,)cioo 12046  [,)cico 12048  volcvol 23039  MblFncmbf 23189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xadd 11823  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-xmet 19560  df-met 19561  df-ovol 23040  df-vol 23041  df-mbf 23194

This theorem is referenced by:  itgaddnclem2  32639