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 37661

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 11176	. . . . 5 ⊢ 0 ∈ ℝ
3		ifcl 4534	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
4	1, 2, 3	sylancl 586	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
5		mbfposadd.4	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)
6		ifcl 4534	. . . . 5 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
7	5, 2, 6	sylancl 586	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
8	4, 7	readdcld 11203	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ)
9	8	fmpttd 7087	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))):𝐴⟶ℝ)
10		ssrab2 4043	. . . 4 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ⊆ 𝐴
11		fssres 6726	. . . 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 4201	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
14		resabs1 5977	. . . . . 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 3930	. . . . . . . . 9 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
17		rabid 3427	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵))
18		rabid 3427	. . . . . . . . . 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 4494	. . . . . . . . . 10 ⊢ (0 ≤ 𝐵 → if(0 ≤ 𝐵, 𝐵, 0) = 𝐵)
22		iftrue 4494	. . . . . . . . . 10 ⊢ (0 ≤ 𝐶 → if(0 ≤ 𝐶, 𝐶, 0) = 𝐶)
23	21, 22	oveqan12d 7406	. . . . . . . . 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 5202	. . . . . 6 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶))
27		inss1 4200	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵}
28		ssrab2 4043	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ⊆ 𝐴
29	27, 28	sstri 3956	. . . . . . 7 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴
30		resmpt 6008	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
31		nfcv 2891	. . . . . . . . . 10 ⊢ Ⅎ𝑦(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
32		nfcsb1v 3886	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
33		csbeq1a 3876	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
34	31, 32, 33	cbvmpt 5209	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
35	34	reseq1i 5946	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
36		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
37		nfrab1 3426	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵}
38		nfrab1 3426	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
39	37, 38	nfin 4187	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
40	39	nfcri 2883	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
41	32	nfeq2 2909	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))
42	40, 41	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
43		eleq1w 2811	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
44	33	eqeq2d 2740	. . . . . . . . . . 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 5181	. . . . . . . . 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 2762	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
50	30, 35, 49	3eqtr4g 2789	. . . . . . 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 6008	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)))
53		nfcv 2891	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝐵 + 𝐶)
54		nfcsb1v 3886	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)
55		csbeq1a 3876	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝐵 + 𝐶) = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
56	53, 54, 55	cbvmpt 5209	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
57	56	reseq1i 5946	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
58		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶))
59	54	nfeq2 2909	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)
60	40, 59	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
61	55	eqeq2d 2740	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = (𝐵 + 𝐶) ↔ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶)))
62	43, 61	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (𝐵 + 𝐶)) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))))
63	58, 60, 62	cbvopab1 5181	. . . . . . . . 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 2762	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(𝐵 + 𝐶))
67	52, 57, 66	3eqtr4g 2789	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶)))
68	29, 67	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (𝐵 + 𝐶))
69	26, 51, 68	3eqtr4i 2762	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
70	15, 69	eqtri 2752	. . . 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 13415	. . . . . . . . . 10 ⊢ (𝐵 ∈ (0[,)+∞) ↔ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵))
74	72, 73	bitr4di 289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ 𝐵 ∈ (0[,)+∞)))
75	74	rabbidva 3412	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)})
76		0xr 11221	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ^*
77		pnfxr 11228	. . . . . . . . . . 11 ⊢ +∞ ∈ ℝ^*
78		0ltpnf 13082	. . . . . . . . . . 11 ⊢ 0 < +∞
79		snunioo 13439	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 0 < +∞) → ({0} ∪ (0(,)+∞)) = (0[,)+∞))
80	76, 77, 78, 79	mp3an 1463	. . . . . . . . . 10 ⊢ ({0} ∪ (0(,)+∞)) = (0[,)+∞)
81	80	imaeq2i 6029	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ ({0} ∪ (0(,)+∞))) = (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0[,)+∞))
82		imaundi 6122	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ ({0} ∪ (0(,)+∞))) = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)))
83		eqid 2729	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
84	83	mptpreima 6211	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0[,)+∞)) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)}
85	81, 82, 84	3eqtr3ri 2761	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (0[,)+∞)} = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)))
86	75, 85	eqtrdi 2780	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞))))
87		mbfposadd.1	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
88	1	fmpttd 7087	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ)
89		mbfimasn 25533	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ ∧ 0 ∈ ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol)
90	2, 89	mp3an3 1452	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ {0}) ∈ dom vol)
91		mbfima 25531	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (0(,)+∞)) ∈ dom vol)
92		unmbl 25438	. . . . . . . . 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 2828	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∈ dom vol)
96	5	biantrurd 532	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)))
97		elrege0 13415	. . . . . . . . . 10 ⊢ (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
98	96, 97	bitr4di 289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ 𝐶 ∈ (0[,)+∞)))
99	98	rabbidva 3412	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)})
100	80	imaeq2i 6029	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ ({0} ∪ (0(,)+∞))) = (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0[,)+∞))
101		imaundi 6122	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ ({0} ∪ (0(,)+∞))) = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)))
102		eqid 2729	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ 𝐶)
103	102	mptpreima 6211	. . . . . . . . 9 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0[,)+∞)) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)}
104	100, 101, 103	3eqtr3ri 2761	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (0[,)+∞)} = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)))
105	99, 104	eqtrdi 2780	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = ((^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∪ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞))))
106		mbfposadd.3	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
107	5	fmpttd 7087	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ)
108		mbfimasn 25533	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ ∧ 0 ∈ ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol)
109	2, 108	mp3an3 1452	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ {0}) ∈ dom vol)
110		mbfima 25531	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (0(,)+∞)) ∈ dom vol)
111		unmbl 25438	. . . . . . . . 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 2828	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol)
115		inmbl 25443	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∈ dom vol ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol) → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
116	95, 114, 115	syl2anc 584	. . . . 5 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
117		mbfres 25545	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ MblFn ∧ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol) → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
118	71, 116, 117	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
119	70, 118	eqeltrid 2832	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
120		inss2 4201	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
121		resabs1 5977	. . . . . 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 628	. . . . . . . . 9 ⊢ ((𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶)))
125		elin 3930	. . . . . . . . 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 4497	. . . . . . . . . . 11 ⊢ (¬ 0 ≤ 𝐵 → if(0 ≤ 𝐵, 𝐵, 0) = 0)
129	128, 22	oveqan12d 7406	. . . . . . . . . 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 11202	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
132	131	addlidd 11375	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 + 𝐶) = 𝐶)
133	132	adantrr 717	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (¬ 0 ≤ 𝐵 ∧ 0 ≤ 𝐶))) → (0 + 𝐶) = 𝐶)
134	130, 133	eqtrd 2764	. . . . . . . 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 5200	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶))
137		inss1 4200	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}
138		ssrab2 4043	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ⊆ 𝐴
139	137, 138	sstri 3956	. . . . . . 7 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴
140		resmpt 6008	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
141	34	reseq1i 5946	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
142		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
143		nfrab1 3426	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}
144	143, 38	nfin 4187	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
145	144	nfcri 2883	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
146	145, 41	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
147		eleq1w 2811	. . . . . . . . . . 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 5181	. . . . . . . . 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 2762	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
153	140, 141, 152	3eqtr4g 2789	. . . . . . 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 6008	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶))
156		nfcv 2891	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐶
157		nfcsb1v 3886	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶
158		csbeq1a 3876	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶)
159	156, 157, 158	cbvmpt 5209	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶)
160	159	reseq1i 5946	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
161		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶)
162	157	nfeq2 2909	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌𝐶
163	145, 162	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)
164	158	eqeq2d 2740	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐶 ↔ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶))
165	147, 164	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = 𝐶) ↔ (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∧ 𝑧 = ⦋𝑦 / 𝑥⦌𝐶)))
166	161, 163, 165	cbvopab1 5181	. . . . . . . . 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 2762	. . . . . . . 8 ⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶) = (𝑦 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ ⦋𝑦 / 𝑥⦌𝐶)
170	155, 160, 169	3eqtr4g 2789	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶))
171	139, 170	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↦ 𝐶)
172	136, 154, 171	3eqtr4g 2789	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
173	122, 172	eqtrid 2776	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})))
174	83	mptpreima 6211	. . . . . . . 8 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (-∞(,)0)}
175		elioomnf 13405	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ^* → (𝐵 ∈ (-∞(,)0) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0)))
176	76, 175	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐵 ∈ (-∞(,)0) ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0))
177	1	biantrurd 532	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 < 0 ↔ (𝐵 ∈ ℝ ∧ 𝐵 < 0)))
178		ltnle 11253	. . . . . . . . . . . 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 3412	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (-∞(,)0)} = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
183	174, 182	eqtrid 2776	. . . . . . 7 ⊢ (𝜑 → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
184		mbfima 25531	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) ∈ dom vol)
185	87, 88, 184	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (^◡(𝑥 ∈ 𝐴 ↦ 𝐵) “ (-∞(,)0)) ∈ dom vol)
186	183, 185	eqeltrrd 2829	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∈ dom vol)
187		inmbl 25443	. . . . . 6 ⊢ (({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∈ dom vol ∧ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∈ dom vol) → ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
188	186, 114, 187	syl2anc 584	. . . . 5 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol)
189		mbfres 25545	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ dom vol) → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
190	106, 188, 189	syl2anc 584	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
191	173, 190	eqeltrd 2828	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ↾ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) ∈ MblFn)
192		ssid 3969	. . . . . 6 ⊢ 𝐴 ⊆ 𝐴
193		dfrab3ss 4286	. . . . . 6 ⊢ (𝐴 ⊆ 𝐴 → {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
194	192, 193	ax-mp 5	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} = (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
195		rabxm 4353	. . . . . 6 ⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵})
196	195	ineq1i 4179	. . . . 5 ⊢ (𝐴 ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) = (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}) ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
197		indir 4249	. . . . 5 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵}) ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) = (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}))
198	194, 196, 197	3eqtrri 2757	. . . 4 ⊢ (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}
199	198	a1i 11	. . 3 ⊢ (𝜑 → (({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∪ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐵} ∩ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})) = {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶})
200	12, 119, 191, 199	mbfres2 25546	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶}) ∈ MblFn)
201		rabid 3427	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ ¬ 0 ≤ 𝐶))
202		iffalse 4497	. . . . . . . . 9 ⊢ (¬ 0 ≤ 𝐶 → if(0 ≤ 𝐶, 𝐶, 0) = 0)
203	202	oveq2d 7403	. . . . . . . 8 ⊢ (¬ 0 ≤ 𝐶 → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) = (if(0 ≤ 𝐵, 𝐵, 0) + 0))
204	4	recnd 11202	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℂ)
205	204	addridd 11374	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + 0) = if(0 ≤ 𝐵, 𝐵, 0))
206	203, 205	sylan9eqr 2786	. . . . . . 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 5200	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)))
210		ssrab2 4043	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴
211		resmpt 6008	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
212	34	reseq1i 5946	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
213		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
214		nfrab1 3426	. . . . . . . . . 10 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}
215	214	nfcri 2883	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}
216	215, 41	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
217		eleq1w 2811	. . . . . . . . 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 5181	. . . . . . 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 2762	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
223	211, 212, 222	3eqtr4g 2789	. . . . 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 6008	. . . . . 6 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ⊆ 𝐴 → ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)))
226		nfcv 2891	. . . . . . . 8 ⊢ Ⅎ𝑦if(0 ≤ 𝐵, 𝐵, 0)
227		nfcsb1v 3886	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)
228		csbeq1a 3876	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → if(0 ≤ 𝐵, 𝐵, 0) = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
229	226, 227, 228	cbvmpt 5209	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
230	229	reseq1i 5946	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑦 ∈ 𝐴 ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
231		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = if(0 ≤ 𝐵, 𝐵, 0))
232	227	nfeq2 2909	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0)
233	215, 232	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∧ 𝑧 = ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
234	228	eqeq2d 2740	. . . . . . . . 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 5181	. . . . . . 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 2762	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ↦ ⦋𝑦 / 𝑥⦌if(0 ≤ 𝐵, 𝐵, 0))
240	225, 230, 239	3eqtr4g 2789	. . . . 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 2789	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}))
243	1, 87	mbfpos 25552	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)
244	102	mptpreima 6211	. . . . . 6 ⊢ (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (-∞(,)0)}
245		elioomnf 13405	. . . . . . . . 9 ⊢ (0 ∈ ℝ^* → (𝐶 ∈ (-∞(,)0) ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0)))
246	76, 245	ax-mp 5	. . . . . . . 8 ⊢ (𝐶 ∈ (-∞(,)0) ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0))
247	5	biantrurd 532	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 < 0 ↔ (𝐶 ∈ ℝ ∧ 𝐶 < 0)))
248		ltnle 11253	. . . . . . . . . 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 3412	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ (-∞(,)0)} = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
253	244, 252	eqtrid 2776	. . . . 5 ⊢ (𝜑 → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) = {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
254		mbfima 25531	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℝ) → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) ∈ dom vol)
255	106, 107, 254	syl2anc 584	. . . . 5 ⊢ (𝜑 → (^◡(𝑥 ∈ 𝐴 ↦ 𝐶) “ (-∞(,)0)) ∈ dom vol)
256	253, 255	eqeltrrd 2829	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶} ∈ dom vol)
257		mbfres 25545	. . . 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 2828	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ↾ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) ∈ MblFn)
260		rabxm 4353	. . . 4 ⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶})
261	260	eqcomi 2738	. . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = 𝐴
262	261	a1i 11	. 2 ⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 0 ≤ 𝐶} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 0 ≤ 𝐶}) = 𝐴)
263	9, 200, 259, 262	mbfres2 25546	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 1540 ∈ wcel 2109 {crab 3405 ⦋csb 3862 ∪ cun 3912 ∩ cin 3913 ⊆ wss 3914 ifcif 4488 {csn 4589 class class class wbr 5107 {copab 5169 ↦ cmpt 5188 ^◡ccnv 5637 dom cdm 5638 ↾ cres 5640 “ cima 5641 ⟶wf 6507 (class class class)co 7387 ℝcr 11067 0cc0 11068 + caddc 11071 +∞cpnf 11205 -∞cmnf 11206 ℝ^*cxr 11207 < clt 11208 ≤ cle 11209 (,)cioo 13306 [,)cico 13308 volcvol 25364 MblFncmbf 25515

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-of 7653 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-er 8671 df-map 8801 df-pm 8802 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-sup 9393 df-inf 9394 df-oi 9463 df-dju 9854 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-n0 12443 df-z 12530 df-uz 12794 df-q 12908 df-rp 12952 df-xadd 13073 df-ioo 13310 df-ico 13312 df-icc 13313 df-fz 13469 df-fzo 13616 df-fl 13754 df-seq 13967 df-exp 14027 df-hash 14296 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-clim 15454 df-sum 15653 df-xmet 21257 df-met 21258 df-ovol 25365 df-vol 25366 df-mbf 25520

This theorem is referenced by: itgaddnclem2 37673

W3C validator