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 37653

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 11260	. . . . 5 ⊢ 0 ∈ ℝ
3		ifcl 4575	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
4	1, 2, 3	sylancl 586	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
5		mbfposadd.4	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)
6		ifcl 4575	. . . . 5 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
7	5, 2, 6	sylancl 586	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
8	4, 7	readdcld 11287	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ)
9	8	fmpttd 7134	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))):𝐴⟶ℝ)
10		ssrab2 4089	. . . 4 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ⊆ 𝐴
11		fssres 6774	. . . 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 4245	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
14		resabs1 6026	. . . . . 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 3978	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
17		rabid 3454	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))
18		rabid 3454	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶))
19	17, 18	anbi12i 628	. . . . . . . . 9 ⊢ ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
20	16, 19	bitri 275	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
21		iftrue 4536	. . . . . . . . . 10 ⊢ (0 ≤ 𝐵 → if(0 ≤ 𝐵, 𝐵, 0) = 𝐵)
22		iftrue 4536	. . . . . . . . . 10 ⊢ (0 ≤ 𝐶 → if(0 ≤ 𝐶, 𝐶, 0) = 𝐶)
23	21, 22	oveqan12d 7449	. . . . . . . . 9 ⊢ ((0 ≤ 𝐵 ∧ 0 ≤ 𝐶) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (𝐵 + 𝐶))
24	23	ad2ant2l 746	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (𝐵 + 𝐶))
25	20, 24	sylbi 217	. . . . . . 7 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (𝐵 + 𝐶))
26	25	mpteq2ia 5250	. . . . . 6 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶))
27		inss1 4244	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵}
28		ssrab2 4089	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ⊆ 𝐴
29	27, 28	sstri 4004	. . . . . . 7 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴
30		resmpt 6056	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
31		nfcv 2902	. . . . . . . . . 10 ⊢ Ⅎ𝑦(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
32		nfcsb1v 3932	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
33		csbeq1a 3921	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
34	31, 32, 33	cbvmpt 5258	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
35	34	reseq1i 5995	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
36		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
37		nfrab1 3453	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵}
38		nfrab1 3453	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
39	37, 38	nfin 4231	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
40	39	nfcri 2894	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
41	32	nfeq2 2920	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
42	40, 41	nfan 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
43		eleq1w 2821	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
44	33	eqeq2d 2745	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
45	43, 44	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))))
46	36, 42, 45	cbvopab1 5222	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
47		df-mpt 5231	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
48		df-mpt 5231	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
49	46, 47, 48	3eqtr4i 2772	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
50	30, 35, 49	3eqtr4g 2799	. . . . . . 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 6056	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)))
53		nfcv 2902	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝐵 + 𝐶)
54		nfcsb1v 3932	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)
55		csbeq1a 3921	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝐵 + 𝐶) = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
56	53, 54, 55	cbvmpt 5258	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
57	56	reseq1i 5995	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
58		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))
59	54	nfeq2 2920	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)
60	40, 59	nfan 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
61	55	eqeq2d 2745	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = (𝐵 + 𝐶) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)))
62	43, 61	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶)) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))))
63	58, 60, 62	cbvopab1 5222	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))}
64		df-mpt 5231	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))}
65		df-mpt 5231	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))}
66	63, 64, 65	3eqtr4i 2772	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
67	52, 57, 66	3eqtr4g 2799	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)))
68	29, 67	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶))
69	26, 51, 68	3eqtr4i 2772	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
70	15, 69	eqtri 2762	. . . 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 13490	. . . . . . . . . 10 ⊢ (𝐵 ∈ (0[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵))
74	72, 73	bitr4di 289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ 𝐵 ∈ (0[,)+∞)))
75	74	rabbidva 3439	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)})
76		0xr 11305	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ^*
77		pnfxr 11312	. . . . . . . . . . 11 ⊢ +∞ ∈ ℝ^*
78		0ltpnf 13161	. . . . . . . . . . 11 ⊢ 0 < +∞
79		snunioo 13514	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 0 < +∞) → ({0} ∪ (0(,)+∞)) = (0[,)+∞))
80	76, 77, 78, 79	mp3an 1460	. . . . . . . . . 10 ⊢ ({0} ∪ (0(,)+∞)) = (0[,)+∞)
81	80	imaeq2i 6077	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ ({0} ∪ (0(,)+∞))) = (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0[,)+∞))
82		imaundi 6171	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ ({0} ∪ (0(,)+∞))) = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)))
83		eqid 2734	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
84	83	mptpreima 6259	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0[,)+∞)) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)}
85	81, 82, 84	3eqtr3ri 2771	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)} = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)))
86	75, 85	eqtrdi 2790	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))))
87		mbfposadd.1	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
88	1	fmpttd 7134	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ)
89		mbfimasn 25680	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ ∧ 0 ∈ ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol)
90	2, 89	mp3an3 1449	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol)
91		mbfima 25678	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)) ∈ dom vol)
92		unmbl 25585	. . . . . . . . 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 532	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)))
97		elrege0 13490	. . . . . . . . . 10 ⊢ (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
98	96, 97	bitr4di 289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ 𝐶 ∈ (0[,)+∞)))
99	98	rabbidva 3439	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)})
100	80	imaeq2i 6077	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ ({0} ∪ (0(,)+∞))) = (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0[,)+∞))
101		imaundi 6171	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ ({0} ∪ (0(,)+∞))) = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)))
102		eqid 2734	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶)
103	102	mptpreima 6259	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0[,)+∞)) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)}
104	100, 101, 103	3eqtr3ri 2771	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)} = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)))
105	99, 104	eqtrdi 2790	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))))
106		mbfposadd.3	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
107	5	fmpttd 7134	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ)
108		mbfimasn 25680	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ ∧ 0 ∈ ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol)
109	2, 108	mp3an3 1449	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol)
110		mbfima 25678	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)) ∈ dom vol)
111		unmbl 25585	. . . . . . . . 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 25590	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∈ dom vol ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol) → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
116	95, 114, 115	syl2anc 584	. . . . 5 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
117		mbfres 25692	. . . . 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 4245	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
121		resabs1 6026	. . . . . 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 3454	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵))
124	123, 18	anbi12i 628	. . . . . . . . 9 ⊢ ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
125		elin 3978	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
126		anandi 676	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
127	124, 125, 126	3bitr4i 303	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶)))
128		iffalse 4539	. . . . . . . . . . 11 ⊢ (¬ 0 ≤ 𝐵 → if(0 ≤ 𝐵, 𝐵, 0) = 0)
129	128, 22	oveqan12d 7449	. . . . . . . . . 10 ⊢ ((¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (0 + 𝐶))
130	129	ad2antll 729	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶))) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (0 + 𝐶))
131	5	recnd 11286	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
132	131	addlidd 11459	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 + 𝐶) = 𝐶)
133	132	adantrr 717	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶))) → (0 + 𝐶) = 𝐶)
134	130, 133	eqtrd 2774	. . . . . . . 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 5247	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶))
137		inss1 4244	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}
138		ssrab2 4089	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ⊆ 𝐴
139	137, 138	sstri 4004	. . . . . . 7 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴
140		resmpt 6056	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
141	34	reseq1i 5995	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
142		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
143		nfrab1 3453	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}
144	143, 38	nfin 4231	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
145	144	nfcri 2894	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
146	145, 41	nfan 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
147		eleq1w 2821	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
148	147, 44	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))))
149	142, 146, 148	cbvopab1 5222	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
150		df-mpt 5231	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
151		df-mpt 5231	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
152	149, 150, 151	3eqtr4i 2772	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
153	140, 141, 152	3eqtr4g 2799	. . . . . . 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 6056	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶))
156		nfcv 2902	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐶
157		nfcsb1v 3932	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶
158		csbeq1a 3921	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶)
159	156, 157, 158	cbvmpt 5258	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶)
160	159	reseq1i 5995	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
161		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)
162	157	nfeq2 2920	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌𝐶
163	145, 162	nfan 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)
164	158	eqeq2d 2745	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐶 ↔ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶))
165	147, 164	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)))
166	161, 163, 165	cbvopab1 5222	. . . . . . . . 9 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)}
167		df-mpt 5231	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)}
168		df-mpt 5231	. . . . . . . . 9 ⊢ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)}
169	166, 167, 168	3eqtr4i 2772	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶)
170	155, 160, 169	3eqtr4g 2799	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶))
171	139, 170	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶)
172	136, 154, 171	3eqtr4g 2799	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
173	122, 172	eqtrid 2786	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
174	83	mptpreima 6259	. . . . . . . 8 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (-∞(,)0)}
175		elioomnf 13480	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ^* → (𝐵 ∈ (-∞(,)0) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0)))
176	76, 175	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐵 ∈ (-∞(,)0) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0))
177	1	biantrurd 532	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 < 0 ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0)))
178		ltnle 11337	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
179	1, 2, 178	sylancl 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
180	177, 179	bitr3d 281	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ ℝ ∧ 𝐵 < 0) ↔ ¬ 0 ≤ 𝐵))
181	176, 180	bitrid 283	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ (-∞(,)0) ↔ ¬ 0 ≤ 𝐵))
182	181	rabbidva 3439	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (-∞(,)0)} = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
183	174, 182	eqtrid 2786	. . . . . . 7 ⊢ (𝜑 → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
184		mbfima 25678	. . . . . . . 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 25590	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∈ dom vol ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol) → ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
188	186, 114, 187	syl2anc 584	. . . . 5 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
189		mbfres 25692	. . . . 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 4017	. . . . . 6 ⊢ 𝐴 ⊆ 𝐴
193		dfrab3ss 4328	. . . . . 6 ⊢ (𝐴 ⊆ 𝐴 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
194	192, 193	ax-mp 5	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
195		rabxm 4395	. . . . . 6 ⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
196	195	ineq1i 4223	. . . . 5 ⊢ (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) = (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}) ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
197		indir 4291	. . . . 5 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}) ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) = (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
198	194, 196, 197	3eqtrri 2767	. . . 4 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
199	198	a1i 11	. . 3 ⊢ (𝜑 → (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
200	12, 119, 191, 199	mbfres2 25693	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ MblFn)
201		rabid 3454	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐶))
202		iffalse 4539	. . . . . . . . 9 ⊢ (¬ 0 ≤ 𝐶 → if(0 ≤ 𝐶, 𝐶, 0) = 0)
203	202	oveq2d 7446	. . . . . . . 8 ⊢ (¬ 0 ≤ 𝐶 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (if(0 ≤ 𝐵, 𝐵, 0) + 0))
204	4	recnd 11286	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℂ)
205	204	addridd 11458	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + 0) = if(0 ≤ 𝐵, 𝐵, 0))
206	203, 205	sylan9eqr 2796	. . . . . . 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 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
209	208	mpteq2dva 5247	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)))
210		ssrab2 4089	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴
211		resmpt 6056	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
212	34	reseq1i 5995	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
213		nfv 1911	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
214		nfrab1 3453	. . . . . . . . . 10 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}
215	214	nfcri 2894	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}
216	215, 41	nfan 1896	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
217		eleq1w 2821	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↔ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}))
218	217, 44	anbi12d 632	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↔ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))))
219	213, 216, 218	cbvopab1 5222	. . . . . . 7 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
220		df-mpt 5231	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
221		df-mpt 5231	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))}
222	219, 220, 221	3eqtr4i 2772	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
223	211, 212, 222	3eqtr4g 2799	. . . . 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 6056	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)))
226		nfcv 2902	. . . . . . . 8 ⊢ Ⅎ𝑦if(0 ≤ 𝐵, 𝐵, 0)
227		nfcsb1v 3932	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)
228		csbeq1a 3921	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → if(0 ≤ 𝐵, 𝐵, 0) = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
229	226, 227, 228	cbvmpt 5258	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
230	229	reseq1i 5995	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
231		nfv 1911	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))
232	227	nfeq2 2920	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)
233	215, 232	nfan 1896	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
234	228	eqeq2d 2745	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑧 = if(0 ≤ 𝐵, 𝐵, 0) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)))
235	217, 234	anbi12d 632	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0)) ↔ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))))
236	231, 233, 235	cbvopab1 5222	. . . . . . 7 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))}
237		df-mpt 5231	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))}
238		df-mpt 5231	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))}
239	236, 237, 238	3eqtr4i 2772	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
240	225, 230, 239	3eqtr4g 2799	. . . . 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 2799	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}))
243	1, 87	mbfpos 25699	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)
244	102	mptpreima 6259	. . . . . 6 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (-∞(,)0)}
245		elioomnf 13480	. . . . . . . . 9 ⊢ (0 ∈ ℝ^* → (𝐶 ∈ (-∞(,)0) ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0)))
246	76, 245	ax-mp 5	. . . . . . . 8 ⊢ (𝐶 ∈ (-∞(,)0) ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0))
247	5	biantrurd 532	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 < 0 ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0)))
248		ltnle 11337	. . . . . . . . . 10 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
249	5, 2, 248	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
250	247, 249	bitr3d 281	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐶 ∈ ℝ ∧ 𝐶 < 0) ↔ ¬ 0 ≤ 𝐶))
251	246, 250	bitrid 283	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ∈ (-∞(,)0) ↔ ¬ 0 ≤ 𝐶))
252	251	rabbidva 3439	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (-∞(,)0)} = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
253	244, 252	eqtrid 2786	. . . . 5 ⊢ (𝜑 → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
254		mbfima 25678	. . . . . 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 25692	. . . 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 4395	. . . 4 ⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
261	260	eqcomi 2743	. . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = 𝐴
262	261	a1i 11	. 2 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = 𝐴)
263	9, 200, 259, 262	mbfres2 25693	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ MblFn)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1536 ∈ wcel 2105 {crab 3432 ⦋csb 3907 ∪ cun 3960 ∩ cin 3961 ⊆ wss 3962 ifcif 4530 {csn 4630 class class class wbr 5147 {copab 5209 ↦ cmpt 5230 ^◡ccnv 5687 dom cdm 5688 ↾ cres 5690 “ cima 5691 ⟶wf 6558 (class class class)co 7430 ℝcr 11151 0cc0 11152 + caddc 11155 +∞cpnf 11289 -∞cmnf 11290 ℝ^*cxr 11291 < clt 11292 ≤ cle 11293 (,)cioo 13383 [,)cico 13385 volcvol 25511 MblFncmbf 25662

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-inf2 9678 ax-cnex 11208 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-addrcl 11213 ax-mulcl 11214 ax-mulrcl 11215 ax-mulcom 11216 ax-addass 11217 ax-mulass 11218 ax-distr 11219 ax-i2m1 11220 ax-1ne0 11221 ax-1rid 11222 ax-rnegex 11223 ax-rrecex 11224 ax-cnre 11225 ax-pre-lttri 11226 ax-pre-lttrn 11227 ax-pre-ltadd 11228 ax-pre-mulgt0 11229 ax-pre-sup 11230

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-int 4951 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-se 5641 df-we 5642 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-pred 6322 df-ord 6388 df-on 6389 df-lim 6390 df-suc 6391 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-isom 6571 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-of 7696 df-om 7887 df-1st 8012 df-2nd 8013 df-frecs 8304 df-wrecs 8335 df-recs 8409 df-rdg 8448 df-1o 8504 df-2o 8505 df-er 8743 df-map 8866 df-pm 8867 df-en 8984 df-dom 8985 df-sdom 8986 df-fin 8987 df-sup 9479 df-inf 9480 df-oi 9547 df-dju 9938 df-card 9976 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11491 df-neg 11492 df-div 11918 df-nn 12264 df-2 12326 df-3 12327 df-n0 12524 df-z 12611 df-uz 12876 df-q 12988 df-rp 13032 df-xadd 13152 df-ioo 13387 df-ico 13389 df-icc 13390 df-fz 13544 df-fzo 13691 df-fl 13828 df-seq 14039 df-exp 14099 df-hash 14366 df-cj 15134 df-re 15135 df-im 15136 df-sqrt 15270 df-abs 15271 df-clim 15520 df-sum 15719 df-xmet 21374 df-met 21375 df-ovol 25512 df-vol 25513 df-mbf 25667

This theorem is referenced by: itgaddnclem2 37665

W3C validator