Theorem mbfposadd 37048

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 11220	. . . . 5 ⊢ 0 ∈ ℝ
3		ifcl 4568	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
4	1, 2, 3	sylancl 585	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
5		mbfposadd.4	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)
6		ifcl 4568	. . . . 5 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
7	5, 2, 6	sylancl 585	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
8	4, 7	readdcld 11247	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ)
9	8	fmpttd 7110	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))):𝐴⟶ℝ)
10		ssrab2 4072	. . . 4 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ⊆ 𝐴
11		fssres 6751	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))):𝐴⟶ℝ ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ⊆ 𝐴) → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}):{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}⟶ℝ)
12	9, 10, 11	sylancl 585	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}):{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}⟶ℝ)
13		inss2 4224	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
14		resabs1 6005	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
15	13, 14	ax-mp 5	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
16		elin 3959	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
17		rabid 3446	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))
18		rabid 3446	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶))
19	17, 18	anbi12i 626	. . . . . . . . 9 ⊢ ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
20	16, 19	bitri 275	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
21		iftrue 4529	. . . . . . . . . 10 ⊢ (0 ≤ 𝐵 → if(0 ≤ 𝐵, 𝐵, 0) = 𝐵)
22		iftrue 4529	. . . . . . . . . 10 ⊢ (0 ≤ 𝐶 → if(0 ≤ 𝐶, 𝐶, 0) = 𝐶)
23	21, 22	oveqan12d 7424	. . . . . . . . 9 ⊢ ((0 ≤ 𝐵 ∧ 0 ≤ 𝐶) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (𝐵 + 𝐶))
24	23	ad2ant2l 743	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (𝐵 + 𝐶))
25	20, 24	sylbi 216	. . . . . . 7 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (𝐵 + 𝐶))
26	25	mpteq2ia 5244	. . . . . 6 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶))
27		inss1 4223	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵}
28		ssrab2 4072	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ⊆ 𝐴
29	27, 28	sstri 3986	. . . . . . 7 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴
30		resmpt 6031	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
31		nfcv 2897	. . . . . . . . . 10 ⊢ Ⅎ𝑦(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
32		nfcsb1v 3913	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
33		csbeq1a 3902	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
34	31, 32, 33	cbvmpt 5252	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
35	34	reseq1i 5971	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
36		nfv 1909	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
37		nfrab1 3445	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵}
38		nfrab1 3445	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
39	37, 38	nfin 4211	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
40	39	nfcri 2884	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
41	32	nfeq2 2914	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
42	40, 41	nfan 1894	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
43		eleq1w 2810	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
44	33	eqeq2d 2737	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
45	43, 44	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))))
46	36, 42, 45	cbvopab1 5216	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
47		df-mpt 5225	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
48		df-mpt 5225	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
49	46, 47, 48	3eqtr4i 2764	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
50	30, 35, 49	3eqtr4g 2791	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
51	29, 50	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
52		resmpt 6031	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)))
53		nfcv 2897	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝐵 + 𝐶)
54		nfcsb1v 3913	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)
55		csbeq1a 3902	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝐵 + 𝐶) = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
56	53, 54, 55	cbvmpt 5252	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
57	56	reseq1i 5971	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
58		nfv 1909	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))
59	54	nfeq2 2914	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)
60	40, 59	nfan 1894	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
61	55	eqeq2d 2737	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = (𝐵 + 𝐶) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)))
62	43, 61	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶)) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))))
63	58, 60, 62	cbvopab1 5216	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))}
64		df-mpt 5225	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))}
65		df-mpt 5225	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))}
66	63, 64, 65	3eqtr4i 2764	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
67	52, 57, 66	3eqtr4g 2791	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)))
68	29, 67	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶))
69	26, 51, 68	3eqtr4i 2764	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
70	15, 69	eqtri 2754	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
71		mbfposadd.5	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)
72	1	biantrurd 532	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)))
73		elrege0 13437	. . . . . . . . . 10 ⊢ (𝐵 ∈ (0[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵))
74	72, 73	bitr4di 289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ 𝐵 ∈ (0[,)+∞)))
75	74	rabbidva 3433	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)})
76		0xr 11265	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ*
77		pnfxr 11272	. . . . . . . . . . 11 ⊢ +∞ ∈ ℝ*
78		0ltpnf 13108	. . . . . . . . . . 11 ⊢ 0 < +∞
79		snunioo 13461	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) → ({0} ∪ (0(,)+∞)) = (0[,)+∞))
80	76, 77, 78, 79	mp3an 1457	. . . . . . . . . 10 ⊢ ({0} ∪ (0(,)+∞)) = (0[,)+∞)
81	80	imaeq2i 6051	. . . . . . . . 9 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ ({0} ∪ (0(,)+∞))) = (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0[,)+∞))
82		imaundi 6143	. . . . . . . . 9 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ ({0} ∪ (0(,)+∞))) = ((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)))
83		eqid 2726	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
84	83	mptpreima 6231	. . . . . . . . 9 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0[,)+∞)) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)}
85	81, 82, 84	3eqtr3ri 2763	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)} = ((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)))
86	75, 85	eqtrdi 2782	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} = ((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))))
87		mbfposadd.1	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
88	1	fmpttd 7110	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ)
89		mbfimasn 25516	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ ∧ 0 ∈ ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol)
90	2, 89	mp3an3 1446	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol)
91		mbfima 25514	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)) ∈ dom vol)
92		unmbl 25421	. . . . . . . . 9 ⊢ (((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol ∧ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)) ∈ dom vol) → ((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))) ∈ dom vol)
93	90, 91, 92	syl2anc 583	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → ((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))) ∈ dom vol)
94	87, 88, 93	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → ((◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))) ∈ dom vol)
95	86, 94	eqeltrd 2827	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∈ dom vol)
96	5	biantrurd 532	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)))
97		elrege0 13437	. . . . . . . . . 10 ⊢ (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
98	96, 97	bitr4di 289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ 𝐶 ∈ (0[,)+∞)))
99	98	rabbidva 3433	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)})
100	80	imaeq2i 6051	. . . . . . . . 9 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ ({0} ∪ (0(,)+∞))) = (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0[,)+∞))
101		imaundi 6143	. . . . . . . . 9 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ ({0} ∪ (0(,)+∞))) = ((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)))
102		eqid 2726	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶)
103	102	mptpreima 6231	. . . . . . . . 9 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0[,)+∞)) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)}
104	100, 101, 103	3eqtr3ri 2763	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)} = ((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)))
105	99, 104	eqtrdi 2782	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = ((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))))
106		mbfposadd.3	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
107	5	fmpttd 7110	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ)
108		mbfimasn 25516	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ ∧ 0 ∈ ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol)
109	2, 108	mp3an3 1446	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol)
110		mbfima 25514	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)) ∈ dom vol)
111		unmbl 25421	. . . . . . . . 9 ⊢ (((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol ∧ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)) ∈ dom vol) → ((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))) ∈ dom vol)
112	109, 110, 111	syl2anc 583	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → ((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))) ∈ dom vol)
113	106, 107, 112	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → ((◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))) ∈ dom vol)
114	105, 113	eqeltrd 2827	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol)
115		inmbl 25426	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∈ dom vol ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol) → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
116	95, 114, 115	syl2anc 583	. . . . 5 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
117		mbfres 25528	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn ∧ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol) → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
118	71, 116, 117	syl2anc 583	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
119	70, 118	eqeltrid 2831	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
120		inss2 4224	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
121		resabs1 6005	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 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 5	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
123		rabid 3446	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵))
124	123, 18	anbi12i 626	. . . . . . . . 9 ⊢ ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
125		elin 3959	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
126		anandi 673	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
127	124, 125, 126	3bitr4i 303	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶)))
128		iffalse 4532	. . . . . . . . . . 11 ⊢ (¬ 0 ≤ 𝐵 → if(0 ≤ 𝐵, 𝐵, 0) = 0)
129	128, 22	oveqan12d 7424	. . . . . . . . . 10 ⊢ ((¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (0 + 𝐶))
130	129	ad2antll 726	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶))) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (0 + 𝐶))
131	5	recnd 11246	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
132	131	addlidd 11419	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 + 𝐶) = 𝐶)
133	132	adantrr 714	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶))) → (0 + 𝐶) = 𝐶)
134	130, 133	eqtrd 2766	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶))) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = 𝐶)
135	127, 134	sylan2b 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = 𝐶)
136	135	mpteq2dva 5241	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶))
137		inss1 4223	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}
138		ssrab2 4072	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ⊆ 𝐴
139	137, 138	sstri 3986	. . . . . . 7 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴
140		resmpt 6031	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
141	34	reseq1i 5971	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
142		nfv 1909	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
143		nfrab1 3445	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}
144	143, 38	nfin 4211	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
145	144	nfcri 2884	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
146	145, 41	nfan 1894	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
147		eleq1w 2810	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
148	147, 44	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))))
149	142, 146, 148	cbvopab1 5216	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
150		df-mpt 5225	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
151		df-mpt 5225	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
152	149, 150, 151	3eqtr4i 2764	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
153	140, 141, 152	3eqtr4g 2791	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
154	139, 153	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
155		resmpt 6031	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶))
156		nfcv 2897	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐶
157		nfcsb1v 3913	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶
158		csbeq1a 3902	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶)
159	156, 157, 158	cbvmpt 5252	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶)
160	159	reseq1i 5971	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
161		nfv 1909	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)
162	157	nfeq2 2914	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌𝐶
163	145, 162	nfan 1894	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)
164	158	eqeq2d 2737	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐶 ↔ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶))
165	147, 164	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)))
166	161, 163, 165	cbvopab1 5216	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)}
167		df-mpt 5225	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)}
168		df-mpt 5225	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)}
169	166, 167, 168	3eqtr4i 2764	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶)
170	155, 160, 169	3eqtr4g 2791	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶))
171	139, 170	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶)
172	136, 154, 171	3eqtr4g 2791	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
173	122, 172	eqtrid 2778	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
174	83	mptpreima 6231	. . . . . . . 8 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (-∞(,)0)}
175		elioomnf 13427	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ* → (𝐵 ∈ (-∞(,)0) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0)))
176	76, 175	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐵 ∈ (-∞(,)0) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0))
177	1	biantrurd 532	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 < 0 ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0)))
178		ltnle 11297	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
179	1, 2, 178	sylancl 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
180	177, 179	bitr3d 281	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ ℝ ∧ 𝐵 < 0) ↔ ¬ 0 ≤ 𝐵))
181	176, 180	bitrid 283	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ (-∞(,)0) ↔ ¬ 0 ≤ 𝐵))
182	181	rabbidva 3433	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (-∞(,)0)} = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
183	174, 182	eqtrid 2778	. . . . . . 7 ⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
184		mbfima 25514	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) ∈ dom vol)
185	87, 88, 184	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) ∈ dom vol)
186	183, 185	eqeltrrd 2828	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∈ dom vol)
187		inmbl 25426	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∈ dom vol ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol) → ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
188	186, 114, 187	syl2anc 583	. . . . 5 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
189		mbfres 25528	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol) → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
190	106, 188, 189	syl2anc 583	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
191	173, 190	eqeltrd 2827	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
192		ssid 3999	. . . . . 6 ⊢ 𝐴 ⊆ 𝐴
193		dfrab3ss 4307	. . . . . 6 ⊢ (𝐴 ⊆ 𝐴 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
194	192, 193	ax-mp 5	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
195		rabxm 4381	. . . . . 6 ⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
196	195	ineq1i 4203	. . . . 5 ⊢ (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) = (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}) ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
197		indir 4270	. . . . 5 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}) ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) = (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
198	194, 196, 197	3eqtrri 2759	. . . 4 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
199	198	a1i 11	. . 3 ⊢ (𝜑 → (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
200	12, 119, 191, 199	mbfres2 25529	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ MblFn)
201		rabid 3446	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐶))
202		iffalse 4532	. . . . . . . . 9 ⊢ (¬ 0 ≤ 𝐶 → if(0 ≤ 𝐶, 𝐶, 0) = 0)
203	202	oveq2d 7421	. . . . . . . 8 ⊢ (¬ 0 ≤ 𝐶 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (if(0 ≤ 𝐵, 𝐵, 0) + 0))
204	4	recnd 11246	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℂ)
205	204	addridd 11418	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + 0) = if(0 ≤ 𝐵, 𝐵, 0))
206	203, 205	sylan9eqr 2788	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 0 ≤ 𝐶) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
207	206	anasss 466	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐶)) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
208	201, 207	sylan2b 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
209	208	mpteq2dva 5241	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)))
210		ssrab2 4072	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴
211		resmpt 6031	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
212	34	reseq1i 5971	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
213		nfv 1909	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
214		nfrab1 3445	. . . . . . . . . 10 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}
215	214	nfcri 2884	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}
216	215, 41	nfan 1894	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
217		eleq1w 2810	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↔ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}))
218	217, 44	anbi12d 630	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↔ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))))
219	213, 216, 218	cbvopab1 5216	. . . . . . 7 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
220		df-mpt 5225	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
221		df-mpt 5225	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
222	219, 220, 221	3eqtr4i 2764	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
223	211, 212, 222	3eqtr4g 2791	. . . . 5 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
224	210, 223	ax-mp 5	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
225		resmpt 6031	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)))
226		nfcv 2897	. . . . . . . 8 ⊢ Ⅎ𝑦if(0 ≤ 𝐵, 𝐵, 0)
227		nfcsb1v 3913	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)
228		csbeq1a 3902	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → if(0 ≤ 𝐵, 𝐵, 0) = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
229	226, 227, 228	cbvmpt 5252	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
230	229	reseq1i 5971	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
231		nfv 1909	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))
232	227	nfeq2 2914	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)
233	215, 232	nfan 1894	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
234	228	eqeq2d 2737	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑧 = if(0 ≤ 𝐵, 𝐵, 0) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)))
235	217, 234	anbi12d 630	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0)) ↔ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))))
236	231, 233, 235	cbvopab1 5216	. . . . . . 7 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))}
237		df-mpt 5225	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))}
238		df-mpt 5225	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))}
239	236, 237, 238	3eqtr4i 2764	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
240	225, 230, 239	3eqtr4g 2791	. . . . 5 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)))
241	210, 240	ax-mp 5	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0))
242	209, 224, 241	3eqtr4g 2791	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}))
243	1, 87	mbfpos 25535	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)
244	102	mptpreima 6231	. . . . . 6 ⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (-∞(,)0)}
245		elioomnf 13427	. . . . . . . . 9 ⊢ (0 ∈ ℝ* → (𝐶 ∈ (-∞(,)0) ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0)))
246	76, 245	ax-mp 5	. . . . . . . 8 ⊢ (𝐶 ∈ (-∞(,)0) ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0))
247	5	biantrurd 532	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 < 0 ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0)))
248		ltnle 11297	. . . . . . . . . 10 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
249	5, 2, 248	sylancl 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
250	247, 249	bitr3d 281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐶 ∈ ℝ ∧ 𝐶 < 0) ↔ ¬ 0 ≤ 𝐶))
251	246, 250	bitrid 283	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ∈ (-∞(,)0) ↔ ¬ 0 ≤ 𝐶))
252	251	rabbidva 3433	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (-∞(,)0)} = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
253	244, 252	eqtrid 2778	. . . . 5 ⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
254		mbfima 25514	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) ∈ dom vol)
255	106, 107, 254	syl2anc 583	. . . . 5 ⊢ (𝜑 → (◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) ∈ dom vol)
256	253, 255	eqeltrrd 2828	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∈ dom vol)
257		mbfres 25528	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∈ dom vol) → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) ∈ MblFn)
258	243, 256, 257	syl2anc 583	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) ∈ MblFn)
259	242, 258	eqeltrd 2827	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) ∈ MblFn)
260		rabxm 4381	. . . 4 ⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
261	260	eqcomi 2735	. . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = 𝐴
262	261	a1i 11	. 2 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = 𝐴)
263	9, 200, 259, 262	mbfres2 25529	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ MblFn)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  {crab 3426  ⦋csb 3888   ∪ cun 3941   ∩ cin 3942   ⊆ wss 3943  ifcif 4523  {csn 4623   class class class wbr 5141  {copab 5203   ↦ cmpt 5224  ^◡ccnv 5668  dom cdm 5669   ↾ cres 5671   “ cima 5672  ⟶wf 6533  (class class class)co 7405  ℝcr 11111  0cc0 11112   + caddc 11115  +∞cpnf 11249  -∞cmnf 11250  ℝ^*cxr 11251   < clt 11252   ≤ cle 11253  (,)cioo 13330  [,)cico 13332  volcvol 25347  MblFncmbf 25498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-q 12937  df-rp 12981  df-xadd 13099  df-ioo 13334  df-ico 13336  df-icc 13337  df-fz 13491  df-fzo 13634  df-fl 13763  df-seq 13973  df-exp 14033  df-hash 14296  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15438  df-sum 15639  df-xmet 21233  df-met 21234  df-ovol 25348  df-vol 25349  df-mbf 25503

This theorem is referenced by:  itgaddnclem2  37060