mbfposadd - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mbfposadd		Structured version Visualization version GIF version

Theorem mbfposadd 36125

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 11157	. . . . 5 ⊢ 0 ∈ ℝ
3		ifcl 4531	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
4	1, 2, 3	sylancl 586	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
5		mbfposadd.4	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)
6		ifcl 4531	. . . . 5 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
7	5, 2, 6	sylancl 586	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
8	4, 7	readdcld 11184	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ)
9	8	fmpttd 7063	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))):𝐴⟶ℝ)
10		ssrab2 4037	. . . 4 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ⊆ 𝐴
11		fssres 6708	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))):𝐴⟶ℝ ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ⊆ 𝐴) → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}):{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}⟶ℝ)
12	9, 10, 11	sylancl 586	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}):{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}⟶ℝ)
13		inss2 4189	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
14		resabs1 5967	. . . . . 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 3926	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
17		rabid 3427	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))
18		rabid 3427	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶))
19	17, 18	anbi12i 627	. . . . . . . . 9 ⊢ ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
20	16, 19	bitri 274	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
21		iftrue 4492	. . . . . . . . . 10 ⊢ (0 ≤ 𝐵 → if(0 ≤ 𝐵, 𝐵, 0) = 𝐵)
22		iftrue 4492	. . . . . . . . . 10 ⊢ (0 ≤ 𝐶 → if(0 ≤ 𝐶, 𝐶, 0) = 𝐶)
23	21, 22	oveqan12d 7376	. . . . . . . . 9 ⊢ ((0 ≤ 𝐵 ∧ 0 ≤ 𝐶) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (𝐵 + 𝐶))
24	23	ad2ant2l 744	. . . . . . . 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 5208	. . . . . 6 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶))
27		inss1 4188	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵}
28		ssrab2 4037	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ⊆ 𝐴
29	27, 28	sstri 3953	. . . . . . 7 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴
30		resmpt 5991	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
31		nfcv 2907	. . . . . . . . . 10 ⊢ Ⅎ𝑦(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
32		nfcsb1v 3880	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
33		csbeq1a 3869	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
34	31, 32, 33	cbvmpt 5216	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
35	34	reseq1i 5933	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
36		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
37		nfrab1 3426	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵}
38		nfrab1 3426	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
39	37, 38	nfin 4176	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
40	39	nfcri 2894	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
41	32	nfeq2 2924	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
42	40, 41	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
43		eleq1w 2820	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
44	33	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
45	43, 44	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))))
46	36, 42, 45	cbvopab1 5180	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
47		df-mpt 5189	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
48		df-mpt 5189	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
49	46, 47, 48	3eqtr4i 2774	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
50	30, 35, 49	3eqtr4g 2801	. . . . . . 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 5991	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)))
53		nfcv 2907	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝐵 + 𝐶)
54		nfcsb1v 3880	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)
55		csbeq1a 3869	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝐵 + 𝐶) = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
56	53, 54, 55	cbvmpt 5216	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
57	56	reseq1i 5933	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
58		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))
59	54	nfeq2 2924	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)
60	40, 59	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
61	55	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = (𝐵 + 𝐶) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)))
62	43, 61	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶)) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))))
63	58, 60, 62	cbvopab1 5180	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))}
64		df-mpt 5189	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))}
65		df-mpt 5189	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))}
66	63, 64, 65	3eqtr4i 2774	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
67	52, 57, 66	3eqtr4g 2801	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)))
68	29, 67	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶))
69	26, 51, 68	3eqtr4i 2774	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
70	15, 69	eqtri 2764	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
71		mbfposadd.5	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn)
72	1	biantrurd 533	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)))
73		elrege0 13371	. . . . . . . . . 10 ⊢ (𝐵 ∈ (0[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵))
74	72, 73	bitr4di 288	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ 𝐵 ∈ (0[,)+∞)))
75	74	rabbidva 3414	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)})
76		0xr 11202	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ^*
77		pnfxr 11209	. . . . . . . . . . 11 ⊢ +∞ ∈ ℝ^*
78		0ltpnf 13043	. . . . . . . . . . 11 ⊢ 0 < +∞
79		snunioo 13395	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 0 < +∞) → ({0} ∪ (0(,)+∞)) = (0[,)+∞))
80	76, 77, 78, 79	mp3an 1461	. . . . . . . . . 10 ⊢ ({0} ∪ (0(,)+∞)) = (0[,)+∞)
81	80	imaeq2i 6011	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ ({0} ∪ (0(,)+∞))) = (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0[,)+∞))
82		imaundi 6102	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ ({0} ∪ (0(,)+∞))) = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)))
83		eqid 2736	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
84	83	mptpreima 6190	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0[,)+∞)) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)}
85	81, 82, 84	3eqtr3ri 2773	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)} = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)))
86	75, 85	eqtrdi 2792	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))))
87		mbfposadd.1	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
88	1	fmpttd 7063	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ)
89		mbfimasn 24996	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ ∧ 0 ∈ ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol)
90	2, 89	mp3an3 1450	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol)
91		mbfima 24994	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)) ∈ dom vol)
92		unmbl 24901	. . . . . . . . 9 ⊢ (((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol ∧ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)) ∈ dom vol) → ((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))) ∈ dom vol)
93	90, 91, 92	syl2anc 584	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → ((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))) ∈ dom vol)
94	87, 88, 93	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))) ∈ dom vol)
95	86, 94	eqeltrd 2838	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∈ dom vol)
96	5	biantrurd 533	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)))
97		elrege0 13371	. . . . . . . . . 10 ⊢ (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
98	96, 97	bitr4di 288	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ 𝐶 ∈ (0[,)+∞)))
99	98	rabbidva 3414	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)})
100	80	imaeq2i 6011	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ ({0} ∪ (0(,)+∞))) = (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0[,)+∞))
101		imaundi 6102	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ ({0} ∪ (0(,)+∞))) = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)))
102		eqid 2736	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶)
103	102	mptpreima 6190	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0[,)+∞)) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)}
104	100, 101, 103	3eqtr3ri 2773	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)} = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)))
105	99, 104	eqtrdi 2792	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))))
106		mbfposadd.3	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
107	5	fmpttd 7063	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ)
108		mbfimasn 24996	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ ∧ 0 ∈ ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol)
109	2, 108	mp3an3 1450	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol)
110		mbfima 24994	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)) ∈ dom vol)
111		unmbl 24901	. . . . . . . . 9 ⊢ (((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol ∧ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)) ∈ dom vol) → ((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))) ∈ dom vol)
112	109, 110, 111	syl2anc 584	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → ((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))) ∈ dom vol)
113	106, 107, 112	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))) ∈ dom vol)
114	105, 113	eqeltrd 2838	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol)
115		inmbl 24906	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∈ dom vol ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol) → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
116	95, 114, 115	syl2anc 584	. . . . 5 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
117		mbfres 25008	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn ∧ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol) → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
118	71, 116, 117	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
119	70, 118	eqeltrid 2842	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
120		inss2 4189	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
121		resabs1 5967	. . . . . 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 3427	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵))
124	123, 18	anbi12i 627	. . . . . . . . 9 ⊢ ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
125		elin 3926	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
126		anandi 674	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
127	124, 125, 126	3bitr4i 302	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶)))
128		iffalse 4495	. . . . . . . . . . 11 ⊢ (¬ 0 ≤ 𝐵 → if(0 ≤ 𝐵, 𝐵, 0) = 0)
129	128, 22	oveqan12d 7376	. . . . . . . . . 10 ⊢ ((¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (0 + 𝐶))
130	129	ad2antll 727	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶))) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (0 + 𝐶))
131	5	recnd 11183	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
132	131	addid2d 11356	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 + 𝐶) = 𝐶)
133	132	adantrr 715	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶))) → (0 + 𝐶) = 𝐶)
134	130, 133	eqtrd 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶))) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = 𝐶)
135	127, 134	sylan2b 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = 𝐶)
136	135	mpteq2dva 5205	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶))
137		inss1 4188	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}
138		ssrab2 4037	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ⊆ 𝐴
139	137, 138	sstri 3953	. . . . . . 7 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴
140		resmpt 5991	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
141	34	reseq1i 5933	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
142		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
143		nfrab1 3426	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}
144	143, 38	nfin 4176	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
145	144	nfcri 2894	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
146	145, 41	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
147		eleq1w 2820	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
148	147, 44	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))))
149	142, 146, 148	cbvopab1 5180	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
150		df-mpt 5189	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
151		df-mpt 5189	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
152	149, 150, 151	3eqtr4i 2774	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
153	140, 141, 152	3eqtr4g 2801	. . . . . . 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 5991	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶))
156		nfcv 2907	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐶
157		nfcsb1v 3880	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶
158		csbeq1a 3869	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶)
159	156, 157, 158	cbvmpt 5216	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶)
160	159	reseq1i 5933	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
161		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)
162	157	nfeq2 2924	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌𝐶
163	145, 162	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)
164	158	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐶 ↔ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶))
165	147, 164	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)))
166	161, 163, 165	cbvopab1 5180	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)}
167		df-mpt 5189	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)}
168		df-mpt 5189	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)}
169	166, 167, 168	3eqtr4i 2774	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶)
170	155, 160, 169	3eqtr4g 2801	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶))
171	139, 170	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶)
172	136, 154, 171	3eqtr4g 2801	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
173	122, 172	eqtrid 2788	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
174	83	mptpreima 6190	. . . . . . . 8 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (-∞(,)0)}
175		elioomnf 13361	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ^* → (𝐵 ∈ (-∞(,)0) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0)))
176	76, 175	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐵 ∈ (-∞(,)0) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0))
177	1	biantrurd 533	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 < 0 ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0)))
178		ltnle 11234	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
179	1, 2, 178	sylancl 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
180	177, 179	bitr3d 280	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ ℝ ∧ 𝐵 < 0) ↔ ¬ 0 ≤ 𝐵))
181	176, 180	bitrid 282	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ (-∞(,)0) ↔ ¬ 0 ≤ 𝐵))
182	181	rabbidva 3414	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (-∞(,)0)} = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
183	174, 182	eqtrid 2788	. . . . . . 7 ⊢ (𝜑 → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
184		mbfima 24994	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) ∈ dom vol)
185	87, 88, 184	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) ∈ dom vol)
186	183, 185	eqeltrrd 2839	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∈ dom vol)
187		inmbl 24906	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∈ dom vol ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol) → ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
188	186, 114, 187	syl2anc 584	. . . . 5 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
189		mbfres 25008	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol) → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
190	106, 188, 189	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
191	173, 190	eqeltrd 2838	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
192		ssid 3966	. . . . . 6 ⊢ 𝐴 ⊆ 𝐴
193		dfrab3ss 4272	. . . . . 6 ⊢ (𝐴 ⊆ 𝐴 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
194	192, 193	ax-mp 5	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
195		rabxm 4346	. . . . . 6 ⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
196	195	ineq1i 4168	. . . . 5 ⊢ (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) = (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}) ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
197		indir 4235	. . . . 5 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}) ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) = (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
198	194, 196, 197	3eqtrri 2769	. . . 4 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
199	198	a1i 11	. . 3 ⊢ (𝜑 → (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
200	12, 119, 191, 199	mbfres2 25009	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ MblFn)
201		rabid 3427	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐶))
202		iffalse 4495	. . . . . . . . 9 ⊢ (¬ 0 ≤ 𝐶 → if(0 ≤ 𝐶, 𝐶, 0) = 0)
203	202	oveq2d 7373	. . . . . . . 8 ⊢ (¬ 0 ≤ 𝐶 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (if(0 ≤ 𝐵, 𝐵, 0) + 0))
204	4	recnd 11183	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℂ)
205	204	addid1d 11355	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + 0) = if(0 ≤ 𝐵, 𝐵, 0))
206	203, 205	sylan9eqr 2798	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 0 ≤ 𝐶) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
207	206	anasss 467	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐶)) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
208	201, 207	sylan2b 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
209	208	mpteq2dva 5205	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)))
210		ssrab2 4037	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴
211		resmpt 5991	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
212	34	reseq1i 5933	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
213		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
214		nfrab1 3426	. . . . . . . . . 10 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}
215	214	nfcri 2894	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}
216	215, 41	nfan 1902	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
217		eleq1w 2820	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↔ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}))
218	217, 44	anbi12d 631	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↔ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))))
219	213, 216, 218	cbvopab1 5180	. . . . . . 7 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
220		df-mpt 5189	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
221		df-mpt 5189	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
222	219, 220, 221	3eqtr4i 2774	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
223	211, 212, 222	3eqtr4g 2801	. . . . 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 5991	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)))
226		nfcv 2907	. . . . . . . 8 ⊢ Ⅎ𝑦if(0 ≤ 𝐵, 𝐵, 0)
227		nfcsb1v 3880	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)
228		csbeq1a 3869	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → if(0 ≤ 𝐵, 𝐵, 0) = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
229	226, 227, 228	cbvmpt 5216	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
230	229	reseq1i 5933	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
231		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))
232	227	nfeq2 2924	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)
233	215, 232	nfan 1902	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
234	228	eqeq2d 2747	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑧 = if(0 ≤ 𝐵, 𝐵, 0) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)))
235	217, 234	anbi12d 631	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0)) ↔ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))))
236	231, 233, 235	cbvopab1 5180	. . . . . . 7 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))}
237		df-mpt 5189	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))}
238		df-mpt 5189	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))}
239	236, 237, 238	3eqtr4i 2774	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
240	225, 230, 239	3eqtr4g 2801	. . . . 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 2801	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}))
243	1, 87	mbfpos 25015	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)
244	102	mptpreima 6190	. . . . . 6 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (-∞(,)0)}
245		elioomnf 13361	. . . . . . . . 9 ⊢ (0 ∈ ℝ^* → (𝐶 ∈ (-∞(,)0) ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0)))
246	76, 245	ax-mp 5	. . . . . . . 8 ⊢ (𝐶 ∈ (-∞(,)0) ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0))
247	5	biantrurd 533	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 < 0 ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0)))
248		ltnle 11234	. . . . . . . . . 10 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
249	5, 2, 248	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
250	247, 249	bitr3d 280	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐶 ∈ ℝ ∧ 𝐶 < 0) ↔ ¬ 0 ≤ 𝐶))
251	246, 250	bitrid 282	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ∈ (-∞(,)0) ↔ ¬ 0 ≤ 𝐶))
252	251	rabbidva 3414	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (-∞(,)0)} = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
253	244, 252	eqtrid 2788	. . . . 5 ⊢ (𝜑 → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
254		mbfima 24994	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) ∈ dom vol)
255	106, 107, 254	syl2anc 584	. . . . 5 ⊢ (𝜑 → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) ∈ dom vol)
256	253, 255	eqeltrrd 2839	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∈ dom vol)
257		mbfres 25008	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∈ dom vol) → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) ∈ MblFn)
258	243, 256, 257	syl2anc 584	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) ∈ MblFn)
259	242, 258	eqeltrd 2838	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) ∈ MblFn)
260		rabxm 4346	. . . 4 ⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
261	260	eqcomi 2745	. . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = 𝐴
262	261	a1i 11	. 2 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = 𝐴)
263	9, 200, 259, 262	mbfres2 25009	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ MblFn)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 {crab 3407 ⦋csb 3855 ∪ cun 3908 ∩ cin 3909 ⊆ wss 3910 ifcif 4486 {csn 4586 class class class wbr 5105 {copab 5167 ↦ cmpt 5188 ^◡ccnv 5632 dom cdm 5633 ↾ cres 5635 “ cima 5636 ⟶wf 6492 (class class class)co 7357 ℝcr 11050 0cc0 11051 + caddc 11054 +∞cpnf 11186 -∞cmnf 11187 ℝ^*cxr 11188 < clt 11189 ≤ cle 11190 (,)cioo 13264 [,)cico 13266 volcvol 24827 MblFncmbf 24978

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-2o 8413 df-er 8648 df-map 8767 df-pm 8768 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9378 df-inf 9379 df-oi 9446 df-dju 9837 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-n0 12414 df-z 12500 df-uz 12764 df-q 12874 df-rp 12916 df-xadd 13034 df-ioo 13268 df-ico 13270 df-icc 13271 df-fz 13425 df-fzo 13568 df-fl 13697 df-seq 13907 df-exp 13968 df-hash 14231 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-clim 15370 df-sum 15571 df-xmet 20789 df-met 20790 df-ovol 24828 df-vol 24829 df-mbf 24983

This theorem is referenced by: itgaddnclem2 36137

W3C validator