Theorem mbfposadd

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)

	Ref	Expression
Hypotheses	mbfposadd.1	$$⊢\phi \to \left(x\in A⟼B\right)\in MblFn$$
	mbfposadd.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	mbfposadd.3	$$⊢\phi \to \left(x\in A⟼C\right)\in MblFn$$
	mbfposadd.4	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℝ$$
	mbfposadd.5	$$⊢\phi \to \left(x\in A⟼B+C\right)\in MblFn$$
Assertion	mbfposadd	$$⊢\phi \to \left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\in MblFn$$

Proof

Step	Hyp	Ref	Expression
1		mbfposadd.1	$$⊢\phi \to \left(x\in A⟼B\right)\in MblFn$$
2		mbfposadd.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
3		mbfposadd.3	$$⊢\phi \to \left(x\in A⟼C\right)\in MblFn$$
4		mbfposadd.4	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℝ$$
5		mbfposadd.5	$$⊢\phi \to \left(x\in A⟼B+C\right)\in MblFn$$
6		0re	$$⊢0\in ℝ$$
7		ifcl	$$⊢\left(B\in ℝ\wedge 0\in ℝ\right)\to if\left(0\le B,B,0\right)\in ℝ$$
8	2 6 7	sylancl	$$⊢\left(\phi \wedge x\in A\right)\to if\left(0\le B,B,0\right)\in ℝ$$
9		ifcl	$$⊢\left(C\in ℝ\wedge 0\in ℝ\right)\to if\left(0\le C,C,0\right)\in ℝ$$
10	4 6 9	sylancl	$$⊢\left(\phi \wedge x\in A\right)\to if\left(0\le C,C,0\right)\in ℝ$$
11	8 10	readdcld	$$⊢\left(\phi \wedge x\in A\right)\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\in ℝ$$
12	11	fmpttd	$$⊢\phi \to \left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right):A⟶ℝ$$
13		ssrab2	$$⊢\left\{x\in A|0\le C\right\}\subseteq A$$
14		fssres	$$⊢\left(\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right):A⟶ℝ\wedge \left\{x\in A|0\le C\right\}\subseteq A\right)\to \left({\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|0\le C\right\}}\right):\left\{x\in A|0\le C\right\}⟶ℝ$$
15	12 13 14	sylancl	$$⊢\phi \to \left({\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|0\le C\right\}}\right):\left\{x\in A|0\le C\right\}⟶ℝ$$
16		inss2	$$⊢\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq \left\{x\in A|0\le C\right\}$$
17		resabs1	$$⊢\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq \left\{x\in A|0\le C\right\}\to {\left({\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|0\le C\right\}}\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}={\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}$$
18	16 17	ax-mp	$$⊢{\left({\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|0\le C\right\}}\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}={\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}$$
19		elin	$$⊢x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\leftrightarrow \left(x\in \left\{x\in A|0\le B\right\}\wedge x\in \left\{x\in A|0\le C\right\}\right)$$
20		rabid	$$⊢x\in \left\{x\in A|0\le B\right\}\leftrightarrow \left(x\in A\wedge 0\le B\right)$$
21		rabid	$$⊢x\in \left\{x\in A|0\le C\right\}\leftrightarrow \left(x\in A\wedge 0\le C\right)$$
22	20 21	anbi12i	$$⊢\left(x\in \left\{x\in A|0\le B\right\}\wedge x\in \left\{x\in A|0\le C\right\}\right)\leftrightarrow \left(\left(x\in A\wedge 0\le B\right)\wedge \left(x\in A\wedge 0\le C\right)\right)$$
23	19 22	bitri	$$⊢x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\leftrightarrow \left(\left(x\in A\wedge 0\le B\right)\wedge \left(x\in A\wedge 0\le C\right)\right)$$
24		iftrue	$$⊢0\le B\to if\left(0\le B,B,0\right)=B$$
25		iftrue	$$⊢0\le C\to if\left(0\le C,C,0\right)=C$$
26	24 25	oveqan12d	$$⊢\left(0\le B\wedge 0\le C\right)\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)=B+C$$
27	26	ad2ant2l	$$⊢\left(\left(x\in A\wedge 0\le B\right)\wedge \left(x\in A\wedge 0\le C\right)\right)\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)=B+C$$
28	23 27	sylbi	$$⊢x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)=B+C$$
29	28	mpteq2ia	$$⊢\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)=\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼B+C\right)$$
30		inss1	$$⊢\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq \left\{x\in A|0\le B\right\}$$
31		ssrab2	$$⊢\left\{x\in A|0\le B\right\}\subseteq A$$
32	30 31	sstri	$$⊢\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq A$$
33		resmpt	$$⊢\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq A\to {\left(y\in A⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}=\left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)$$
34		nfcv	$$⊢\underset{\_}{Ⅎ}y\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
35		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
36		csbeq1a	$$⊢x=y\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
37	34 35 36	cbvmpt	$$⊢\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)=\left(y\in A⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)$$
38	37	reseq1i	$$⊢{\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}={\left(y\in A⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}$$
39		nfv	$$⊢Ⅎy\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
40		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|0\le B\right\}$$
41		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|0\le C\right\}$$
42	40 41	nfin	$$⊢\underset{\_}{Ⅎ}x\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)$$
43	42	nfcri	$$⊢Ⅎxy\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)$$
44	35	nfeq2	$$⊢Ⅎxz=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
45	43 44	nfan	$$⊢Ⅎx\left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)$$
46		eleq1w	$$⊢x=y\to \left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\leftrightarrow y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\right)$$
47	36	eqeq2d	$$⊢x=y\to \left(z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\leftrightarrow z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)$$
48	46 47	anbi12d	$$⊢x=y\to \left(\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\leftrightarrow \left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\right)$$
49	39 45 48	cbvopab1	$$⊢\left\{⟨x,z⟩|\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right\}=\left\{⟨y,z⟩|\left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\right\}$$
50		df-mpt	$$⊢\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)=\left\{⟨x,z⟩|\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right\}$$
51		df-mpt	$$⊢\left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)=\left\{⟨y,z⟩|\left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\right\}$$
52	49 50 51	3eqtr4i	$$⊢\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)=\left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)$$
53	33 38 52	3eqtr4g	$$⊢\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq A\to {\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}=\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
54	32 53	ax-mp	$$⊢{\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}=\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
55		resmpt	$$⊢\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq A\to {\left(y\in A⟼⦋y/x⦌\left(B+C\right)\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}=\left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼⦋y/x⦌\left(B+C\right)\right)$$
56		nfcv	$$⊢\underset{\_}{Ⅎ}y\left(B+C\right)$$
57		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌\left(B+C\right)$$
58		csbeq1a	$$⊢x=y\to B+C=⦋y/x⦌\left(B+C\right)$$
59	56 57 58	cbvmpt	$$⊢\left(x\in A⟼B+C\right)=\left(y\in A⟼⦋y/x⦌\left(B+C\right)\right)$$
60	59	reseq1i	$$⊢{\left(x\in A⟼B+C\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}={\left(y\in A⟼⦋y/x⦌\left(B+C\right)\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}$$
61		nfv	$$⊢Ⅎy\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=B+C\right)$$
62	57	nfeq2	$$⊢Ⅎxz=⦋y/x⦌\left(B+C\right)$$
63	43 62	nfan	$$⊢Ⅎx\left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌\left(B+C\right)\right)$$
64	58	eqeq2d	$$⊢x=y\to \left(z=B+C\leftrightarrow z=⦋y/x⦌\left(B+C\right)\right)$$
65	46 64	anbi12d	$$⊢x=y\to \left(\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=B+C\right)\leftrightarrow \left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌\left(B+C\right)\right)\right)$$
66	61 63 65	cbvopab1	$$⊢\left\{⟨x,z⟩|\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=B+C\right)\right\}=\left\{⟨y,z⟩|\left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌\left(B+C\right)\right)\right\}$$
67		df-mpt	$$⊢\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼B+C\right)=\left\{⟨x,z⟩|\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=B+C\right)\right\}$$
68		df-mpt	$$⊢\left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼⦋y/x⦌\left(B+C\right)\right)=\left\{⟨y,z⟩|\left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌\left(B+C\right)\right)\right\}$$
69	66 67 68	3eqtr4i	$$⊢\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼B+C\right)=\left(y\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼⦋y/x⦌\left(B+C\right)\right)$$
70	55 60 69	3eqtr4g	$$⊢\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq A\to {\left(x\in A⟼B+C\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}=\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼B+C\right)$$
71	32 70	ax-mp	$$⊢{\left(x\in A⟼B+C\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}=\left(x\in \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼B+C\right)$$
72	29 54 71	3eqtr4i	$$⊢{\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}={\left(x\in A⟼B+C\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}$$
73	18 72	eqtri	$$⊢{\left({\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|0\le C\right\}}\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}={\left(x\in A⟼B+C\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}$$
74	2	biantrurd	$$⊢\left(\phi \wedge x\in A\right)\to \left(0\le B\leftrightarrow \left(B\in ℝ\wedge 0\le B\right)\right)$$
75		elrege0	$$⊢B\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(B\in ℝ\wedge 0\le B\right)$$
76	74 75	bitr4di	$$⊢\left(\phi \wedge x\in A\right)\to \left(0\le B\leftrightarrow B\in \left[0,\mathrm{+\infty }\right)\right)$$
77	76	rabbidva	$$⊢\phi \to \left\{x\in A|0\le B\right\}=\left\{x\in A|B\in \left[0,\mathrm{+\infty }\right)\right\}$$
78		0xr	$$⊢0\in {ℝ}^{*}$$
79		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
80		0ltpnf	$$⊢0<\mathrm{+\infty }$$
81		snunioo	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge 0<\mathrm{+\infty }\right)\to \left\{0\right\}\cup \left(0,\mathrm{+\infty }\right)=\left[0,\mathrm{+\infty }\right)$$
82	78 79 80 81	mp3an	$$⊢\left\{0\right\}\cup \left(0,\mathrm{+\infty }\right)=\left[0,\mathrm{+\infty }\right)$$
83	82	imaeq2i	$$⊢{\left(x\in A⟼B\right)}^{-1}\left[\left\{0\right\}\cup \left(0,\mathrm{+\infty }\right)\right]={\left(x\in A⟼B\right)}^{-1}\left[\left[0,\mathrm{+\infty }\right)\right]$$
84		imaundi	$$⊢{\left(x\in A⟼B\right)}^{-1}\left[\left\{0\right\}\cup \left(0,\mathrm{+\infty }\right)\right]={\left(x\in A⟼B\right)}^{-1}\left[\left\{0\right\}\right]\cup {\left(x\in A⟼B\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]$$
85		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
86	85	mptpreima	$$⊢{\left(x\in A⟼B\right)}^{-1}\left[\left[0,\mathrm{+\infty }\right)\right]=\left\{x\in A|B\in \left[0,\mathrm{+\infty }\right)\right\}$$
87	83 84 86	3eqtr3ri	$$⊢\left\{x\in A|B\in \left[0,\mathrm{+\infty }\right)\right\}={\left(x\in A⟼B\right)}^{-1}\left[\left\{0\right\}\right]\cup {\left(x\in A⟼B\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]$$
88	77 87	eqtrdi	$$⊢\phi \to \left\{x\in A|0\le B\right\}={\left(x\in A⟼B\right)}^{-1}\left[\left\{0\right\}\right]\cup {\left(x\in A⟼B\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]$$
89	2	fmpttd	$$⊢\phi \to \left(x\in A⟼B\right):A⟶ℝ$$
90		mbfimasn	$$⊢\left(\left(x\in A⟼B\right)\in MblFn\wedge \left(x\in A⟼B\right):A⟶ℝ\wedge 0\in ℝ\right)\to {\left(x\in A⟼B\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{dom}vol$$
91	6 90	mp3an3	$$⊢\left(\left(x\in A⟼B\right)\in MblFn\wedge \left(x\in A⟼B\right):A⟶ℝ\right)\to {\left(x\in A⟼B\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{dom}vol$$
92		mbfima	$$⊢\left(\left(x\in A⟼B\right)\in MblFn\wedge \left(x\in A⟼B\right):A⟶ℝ\right)\to {\left(x\in A⟼B\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$$
93		unmbl	$$⊢\left({\left(x\in A⟼B\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{dom}vol\wedge {\left(x\in A⟼B\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol\right)\to {\left(x\in A⟼B\right)}^{-1}\left[\left\{0\right\}\right]\cup {\left(x\in A⟼B\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$$
94	91 92 93	syl2anc	$$⊢\left(\left(x\in A⟼B\right)\in MblFn\wedge \left(x\in A⟼B\right):A⟶ℝ\right)\to {\left(x\in A⟼B\right)}^{-1}\left[\left\{0\right\}\right]\cup {\left(x\in A⟼B\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$$
95	1 89 94	syl2anc	$$⊢\phi \to {\left(x\in A⟼B\right)}^{-1}\left[\left\{0\right\}\right]\cup {\left(x\in A⟼B\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$$
96	88 95	eqeltrd	$$⊢\phi \to \left\{x\in A|0\le B\right\}\in \mathrm{dom}vol$$
97	4	biantrurd	$$⊢\left(\phi \wedge x\in A\right)\to \left(0\le C\leftrightarrow \left(C\in ℝ\wedge 0\le C\right)\right)$$
98		elrege0	$$⊢C\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(C\in ℝ\wedge 0\le C\right)$$
99	97 98	bitr4di	$$⊢\left(\phi \wedge x\in A\right)\to \left(0\le C\leftrightarrow C\in \left[0,\mathrm{+\infty }\right)\right)$$
100	99	rabbidva	$$⊢\phi \to \left\{x\in A|0\le C\right\}=\left\{x\in A|C\in \left[0,\mathrm{+\infty }\right)\right\}$$
101	82	imaeq2i	$$⊢{\left(x\in A⟼C\right)}^{-1}\left[\left\{0\right\}\cup \left(0,\mathrm{+\infty }\right)\right]={\left(x\in A⟼C\right)}^{-1}\left[\left[0,\mathrm{+\infty }\right)\right]$$
102		imaundi	$$⊢{\left(x\in A⟼C\right)}^{-1}\left[\left\{0\right\}\cup \left(0,\mathrm{+\infty }\right)\right]={\left(x\in A⟼C\right)}^{-1}\left[\left\{0\right\}\right]\cup {\left(x\in A⟼C\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]$$
103		eqid	$$⊢\left(x\in A⟼C\right)=\left(x\in A⟼C\right)$$
104	103	mptpreima	$$⊢{\left(x\in A⟼C\right)}^{-1}\left[\left[0,\mathrm{+\infty }\right)\right]=\left\{x\in A|C\in \left[0,\mathrm{+\infty }\right)\right\}$$
105	101 102 104	3eqtr3ri	$$⊢\left\{x\in A|C\in \left[0,\mathrm{+\infty }\right)\right\}={\left(x\in A⟼C\right)}^{-1}\left[\left\{0\right\}\right]\cup {\left(x\in A⟼C\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]$$
106	100 105	eqtrdi	$$⊢\phi \to \left\{x\in A|0\le C\right\}={\left(x\in A⟼C\right)}^{-1}\left[\left\{0\right\}\right]\cup {\left(x\in A⟼C\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]$$
107	4	fmpttd	$$⊢\phi \to \left(x\in A⟼C\right):A⟶ℝ$$
108		mbfimasn	$$⊢\left(\left(x\in A⟼C\right)\in MblFn\wedge \left(x\in A⟼C\right):A⟶ℝ\wedge 0\in ℝ\right)\to {\left(x\in A⟼C\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{dom}vol$$
109	6 108	mp3an3	$$⊢\left(\left(x\in A⟼C\right)\in MblFn\wedge \left(x\in A⟼C\right):A⟶ℝ\right)\to {\left(x\in A⟼C\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{dom}vol$$
110		mbfima	$$⊢\left(\left(x\in A⟼C\right)\in MblFn\wedge \left(x\in A⟼C\right):A⟶ℝ\right)\to {\left(x\in A⟼C\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$$
111		unmbl	$$⊢\left({\left(x\in A⟼C\right)}^{-1}\left[\left\{0\right\}\right]\in \mathrm{dom}vol\wedge {\left(x\in A⟼C\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol\right)\to {\left(x\in A⟼C\right)}^{-1}\left[\left\{0\right\}\right]\cup {\left(x\in A⟼C\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$$
112	109 110 111	syl2anc	$$⊢\left(\left(x\in A⟼C\right)\in MblFn\wedge \left(x\in A⟼C\right):A⟶ℝ\right)\to {\left(x\in A⟼C\right)}^{-1}\left[\left\{0\right\}\right]\cup {\left(x\in A⟼C\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$$
113	3 107 112	syl2anc	$$⊢\phi \to {\left(x\in A⟼C\right)}^{-1}\left[\left\{0\right\}\right]\cup {\left(x\in A⟼C\right)}^{-1}\left[\left(0,\mathrm{+\infty }\right)\right]\in \mathrm{dom}vol$$
114	106 113	eqeltrd	$$⊢\phi \to \left\{x\in A|0\le C\right\}\in \mathrm{dom}vol$$
115		inmbl	$$⊢\left(\left\{x\in A|0\le B\right\}\in \mathrm{dom}vol\wedge \left\{x\in A|0\le C\right\}\in \mathrm{dom}vol\right)\to \left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\in \mathrm{dom}vol$$
116	96 114 115	syl2anc	$$⊢\phi \to \left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\in \mathrm{dom}vol$$
117		mbfres	$$⊢\left(\left(x\in A⟼B+C\right)\in MblFn\wedge \left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\in \mathrm{dom}vol\right)\to {\left(x\in A⟼B+C\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}\in MblFn$$
118	5 116 117	syl2anc	$$⊢\phi \to {\left(x\in A⟼B+C\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}\in MblFn$$
119	73 118	eqeltrid	$$⊢\phi \to {\left({\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|0\le C\right\}}\right)\upharpoonright }_{\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}\in MblFn$$
120		inss2	$$⊢\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq \left\{x\in A|0\le C\right\}$$
121		resabs1	$$⊢\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq \left\{x\in A|0\le C\right\}\to {\left({\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|0\le C\right\}}\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}={\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}$$
122	120 121	ax-mp	$$⊢{\left({\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|0\le C\right\}}\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}={\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}$$
123		rabid	$$⊢x\in \left\{x\in A|\neg 0\le B\right\}\leftrightarrow \left(x\in A\wedge \neg 0\le B\right)$$
124	123 21	anbi12i	$$⊢\left(x\in \left\{x\in A|\neg 0\le B\right\}\wedge x\in \left\{x\in A|0\le C\right\}\right)\leftrightarrow \left(\left(x\in A\wedge \neg 0\le B\right)\wedge \left(x\in A\wedge 0\le C\right)\right)$$
125		elin	$$⊢x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\leftrightarrow \left(x\in \left\{x\in A|\neg 0\le B\right\}\wedge x\in \left\{x\in A|0\le C\right\}\right)$$
126		anandi	$$⊢\left(x\in A\wedge \left(\neg 0\le B\wedge 0\le C\right)\right)\leftrightarrow \left(\left(x\in A\wedge \neg 0\le B\right)\wedge \left(x\in A\wedge 0\le C\right)\right)$$
127	124 125 126	3bitr4i	$$⊢x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\leftrightarrow \left(x\in A\wedge \left(\neg 0\le B\wedge 0\le C\right)\right)$$
128		iffalse	$$⊢\neg 0\le B\to if\left(0\le B,B,0\right)=0$$
129	128 25	oveqan12d	$$⊢\left(\neg 0\le B\wedge 0\le C\right)\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)=0+C$$
130	129	ad2antll	$$⊢\left(\phi \wedge \left(x\in A\wedge \left(\neg 0\le B\wedge 0\le C\right)\right)\right)\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)=0+C$$
131	4	recnd	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℂ$$
132	131	addlidd	$$⊢\left(\phi \wedge x\in A\right)\to 0+C=C$$
133	132	adantrr	$$⊢\left(\phi \wedge \left(x\in A\wedge \left(\neg 0\le B\wedge 0\le C\right)\right)\right)\to 0+C=C$$
134	130 133	eqtrd	$$⊢\left(\phi \wedge \left(x\in A\wedge \left(\neg 0\le B\wedge 0\le C\right)\right)\right)\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)=C$$
135	127 134	sylan2b	$$⊢\left(\phi \wedge x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\right)\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)=C$$
136	135	mpteq2dva	$$⊢\phi \to \left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)=\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼C\right)$$
137		inss1	$$⊢\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq \left\{x\in A|\neg 0\le B\right\}$$
138		ssrab2	$$⊢\left\{x\in A|\neg 0\le B\right\}\subseteq A$$
139	137 138	sstri	$$⊢\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq A$$
140		resmpt	$$⊢\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq A\to {\left(y\in A⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}=\left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)$$
141	37	reseq1i	$$⊢{\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}={\left(y\in A⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}$$
142		nfv	$$⊢Ⅎy\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
143		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|\neg 0\le B\right\}$$
144	143 41	nfin	$$⊢\underset{\_}{Ⅎ}x\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)$$
145	144	nfcri	$$⊢Ⅎxy\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)$$
146	145 44	nfan	$$⊢Ⅎx\left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)$$
147		eleq1w	$$⊢x=y\to \left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\leftrightarrow y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\right)$$
148	147 47	anbi12d	$$⊢x=y\to \left(\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\leftrightarrow \left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\right)$$
149	142 146 148	cbvopab1	$$⊢\left\{⟨x,z⟩|\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right\}=\left\{⟨y,z⟩|\left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\right\}$$
150		df-mpt	$$⊢\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)=\left\{⟨x,z⟩|\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right\}$$
151		df-mpt	$$⊢\left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)=\left\{⟨y,z⟩|\left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\right\}$$
152	149 150 151	3eqtr4i	$$⊢\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)=\left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)$$
153	140 141 152	3eqtr4g	$$⊢\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq A\to {\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}=\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
154	139 153	ax-mp	$$⊢{\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}=\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
155		resmpt	$$⊢\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq A\to {\left(y\in A⟼⦋y/x⦌C\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}=\left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼⦋y/x⦌C\right)$$
156		nfcv	$$⊢\underset{\_}{Ⅎ}yC$$
157		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌C$$
158		csbeq1a	$$⊢x=y\to C=⦋y/x⦌C$$
159	156 157 158	cbvmpt	$$⊢\left(x\in A⟼C\right)=\left(y\in A⟼⦋y/x⦌C\right)$$
160	159	reseq1i	$$⊢{\left(x\in A⟼C\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}={\left(y\in A⟼⦋y/x⦌C\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}$$
161		nfv	$$⊢Ⅎy\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=C\right)$$
162	157	nfeq2	$$⊢Ⅎxz=⦋y/x⦌C$$
163	145 162	nfan	$$⊢Ⅎx\left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌C\right)$$
164	158	eqeq2d	$$⊢x=y\to \left(z=C\leftrightarrow z=⦋y/x⦌C\right)$$
165	147 164	anbi12d	$$⊢x=y\to \left(\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=C\right)\leftrightarrow \left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌C\right)\right)$$
166	161 163 165	cbvopab1	$$⊢\left\{⟨x,z⟩|\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=C\right)\right\}=\left\{⟨y,z⟩|\left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌C\right)\right\}$$
167		df-mpt	$$⊢\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼C\right)=\left\{⟨x,z⟩|\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=C\right)\right\}$$
168		df-mpt	$$⊢\left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼⦋y/x⦌C\right)=\left\{⟨y,z⟩|\left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\wedge z=⦋y/x⦌C\right)\right\}$$
169	166 167 168	3eqtr4i	$$⊢\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼C\right)=\left(y\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼⦋y/x⦌C\right)$$
170	155 160 169	3eqtr4g	$$⊢\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\subseteq A\to {\left(x\in A⟼C\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}=\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼C\right)$$
171	139 170	ax-mp	$$⊢{\left(x\in A⟼C\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}=\left(x\in \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)⟼C\right)$$
172	136 154 171	3eqtr4g	$$⊢\phi \to {\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}={\left(x\in A⟼C\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}$$
173	122 172	eqtrid	$$⊢\phi \to {\left({\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|0\le C\right\}}\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}={\left(x\in A⟼C\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}$$
174	85	mptpreima	$$⊢{\left(x\in A⟼B\right)}^{-1}\left[\left(\mathrm{-\infty },0\right)\right]=\left\{x\in A|B\in \left(\mathrm{-\infty },0\right)\right\}$$
175		elioomnf	$$⊢0\in {ℝ}^{*}\to \left(B\in \left(\mathrm{-\infty },0\right)\leftrightarrow \left(B\in ℝ\wedge B<0\right)\right)$$
176	78 175	ax-mp	$$⊢B\in \left(\mathrm{-\infty },0\right)\leftrightarrow \left(B\in ℝ\wedge B<0\right)$$
177	2	biantrurd	$$⊢\left(\phi \wedge x\in A\right)\to \left(B<0\leftrightarrow \left(B\in ℝ\wedge B<0\right)\right)$$
178		ltnle	$$⊢\left(B\in ℝ\wedge 0\in ℝ\right)\to \left(B<0\leftrightarrow \neg 0\le B\right)$$
179	2 6 178	sylancl	$$⊢\left(\phi \wedge x\in A\right)\to \left(B<0\leftrightarrow \neg 0\le B\right)$$
180	177 179	bitr3d	$$⊢\left(\phi \wedge x\in A\right)\to \left(\left(B\in ℝ\wedge B<0\right)\leftrightarrow \neg 0\le B\right)$$
181	176 180	bitrid	$$⊢\left(\phi \wedge x\in A\right)\to \left(B\in \left(\mathrm{-\infty },0\right)\leftrightarrow \neg 0\le B\right)$$
182	181	rabbidva	$$⊢\phi \to \left\{x\in A|B\in \left(\mathrm{-\infty },0\right)\right\}=\left\{x\in A|\neg 0\le B\right\}$$
183	174 182	eqtrid	$$⊢\phi \to {\left(x\in A⟼B\right)}^{-1}\left[\left(\mathrm{-\infty },0\right)\right]=\left\{x\in A|\neg 0\le B\right\}$$
184		mbfima	$$⊢\left(\left(x\in A⟼B\right)\in MblFn\wedge \left(x\in A⟼B\right):A⟶ℝ\right)\to {\left(x\in A⟼B\right)}^{-1}\left[\left(\mathrm{-\infty },0\right)\right]\in \mathrm{dom}vol$$
185	1 89 184	syl2anc	$$⊢\phi \to {\left(x\in A⟼B\right)}^{-1}\left[\left(\mathrm{-\infty },0\right)\right]\in \mathrm{dom}vol$$
186	183 185	eqeltrrd	$$⊢\phi \to \left\{x\in A|\neg 0\le B\right\}\in \mathrm{dom}vol$$
187		inmbl	$$⊢\left(\left\{x\in A|\neg 0\le B\right\}\in \mathrm{dom}vol\wedge \left\{x\in A|0\le C\right\}\in \mathrm{dom}vol\right)\to \left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\in \mathrm{dom}vol$$
188	186 114 187	syl2anc	$$⊢\phi \to \left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\in \mathrm{dom}vol$$
189		mbfres	$$⊢\left(\left(x\in A⟼C\right)\in MblFn\wedge \left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\in \mathrm{dom}vol\right)\to {\left(x\in A⟼C\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}\in MblFn$$
190	3 188 189	syl2anc	$$⊢\phi \to {\left(x\in A⟼C\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}\in MblFn$$
191	173 190	eqeltrd	$$⊢\phi \to {\left({\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|0\le C\right\}}\right)\upharpoonright }_{\left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)}\in MblFn$$
192		ssid	$$⊢A\subseteq A$$
193		dfrab3ss	$$⊢A\subseteq A\to \left\{x\in A|0\le C\right\}=A\cap \left\{x\in A|0\le C\right\}$$
194	192 193	ax-mp	$$⊢\left\{x\in A|0\le C\right\}=A\cap \left\{x\in A|0\le C\right\}$$
195		rabxm	$$⊢A=\left\{x\in A|0\le B\right\}\cup \left\{x\in A|\neg 0\le B\right\}$$
196	195	ineq1i	$$⊢A\cap \left\{x\in A|0\le C\right\}=\left(\left\{x\in A|0\le B\right\}\cup \left\{x\in A|\neg 0\le B\right\}\right)\cap \left\{x\in A|0\le C\right\}$$
197		indir	$$⊢\left(\left\{x\in A|0\le B\right\}\cup \left\{x\in A|\neg 0\le B\right\}\right)\cap \left\{x\in A|0\le C\right\}=\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\cup \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)$$
198	194 196 197	3eqtrri	$$⊢\left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\cup \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)=\left\{x\in A|0\le C\right\}$$
199	198	a1i	$$⊢\phi \to \left(\left\{x\in A|0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)\cup \left(\left\{x\in A|\neg 0\le B\right\}\cap \left\{x\in A|0\le C\right\}\right)=\left\{x\in A|0\le C\right\}$$
200	15 119 191 199	mbfres2	$$⊢\phi \to {\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|0\le C\right\}}\in MblFn$$
201		rabid	$$⊢x\in \left\{x\in A|\neg 0\le C\right\}\leftrightarrow \left(x\in A\wedge \neg 0\le C\right)$$
202		iffalse	$$⊢\neg 0\le C\to if\left(0\le C,C,0\right)=0$$
203	202	oveq2d	$$⊢\neg 0\le C\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)=if\left(0\le B,B,0\right)+0$$
204	8	recnd	$$⊢\left(\phi \wedge x\in A\right)\to if\left(0\le B,B,0\right)\in ℂ$$
205	204	addridd	$$⊢\left(\phi \wedge x\in A\right)\to if\left(0\le B,B,0\right)+0=if\left(0\le B,B,0\right)$$
206	203 205	sylan9eqr	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge \neg 0\le C\right)\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)=if\left(0\le B,B,0\right)$$
207	206	anasss	$$⊢\left(\phi \wedge \left(x\in A\wedge \neg 0\le C\right)\right)\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)=if\left(0\le B,B,0\right)$$
208	201 207	sylan2b	$$⊢\left(\phi \wedge x\in \left\{x\in A|\neg 0\le C\right\}\right)\to if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)=if\left(0\le B,B,0\right)$$
209	208	mpteq2dva	$$⊢\phi \to \left(x\in \left\{x\in A|\neg 0\le C\right\}⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)=\left(x\in \left\{x\in A|\neg 0\le C\right\}⟼if\left(0\le B,B,0\right)\right)$$
210		ssrab2	$$⊢\left\{x\in A|\neg 0\le C\right\}\subseteq A$$
211		resmpt	$$⊢\left\{x\in A|\neg 0\le C\right\}\subseteq A\to {\left(y\in A⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}=\left(y\in \left\{x\in A|\neg 0\le C\right\}⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)$$
212	37	reseq1i	$$⊢{\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}={\left(y\in A⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}$$
213		nfv	$$⊢Ⅎy\left(x\in \left\{x\in A|\neg 0\le C\right\}\wedge z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
214		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|\neg 0\le C\right\}$$
215	214	nfcri	$$⊢Ⅎxy\in \left\{x\in A|\neg 0\le C\right\}$$
216	215 44	nfan	$$⊢Ⅎx\left(y\in \left\{x\in A|\neg 0\le C\right\}\wedge z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)$$
217		eleq1w	$$⊢x=y\to \left(x\in \left\{x\in A|\neg 0\le C\right\}\leftrightarrow y\in \left\{x\in A|\neg 0\le C\right\}\right)$$
218	217 47	anbi12d	$$⊢x=y\to \left(\left(x\in \left\{x\in A|\neg 0\le C\right\}\wedge z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\leftrightarrow \left(y\in \left\{x\in A|\neg 0\le C\right\}\wedge z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\right)$$
219	213 216 218	cbvopab1	$$⊢\left\{⟨x,z⟩|\left(x\in \left\{x\in A|\neg 0\le C\right\}\wedge z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right\}=\left\{⟨y,z⟩|\left(y\in \left\{x\in A|\neg 0\le C\right\}\wedge z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\right\}$$
220		df-mpt	$$⊢\left(x\in \left\{x\in A|\neg 0\le C\right\}⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)=\left\{⟨x,z⟩|\left(x\in \left\{x\in A|\neg 0\le C\right\}\wedge z=if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right\}$$
221		df-mpt	$$⊢\left(y\in \left\{x\in A|\neg 0\le C\right\}⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)=\left\{⟨y,z⟩|\left(y\in \left\{x\in A|\neg 0\le C\right\}\wedge z=⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)\right\}$$
222	219 220 221	3eqtr4i	$$⊢\left(x\in \left\{x\in A|\neg 0\le C\right\}⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)=\left(y\in \left\{x\in A|\neg 0\le C\right\}⟼⦋y/x⦌\left(if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\right)$$
223	211 212 222	3eqtr4g	$$⊢\left\{x\in A|\neg 0\le C\right\}\subseteq A\to {\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}=\left(x\in \left\{x\in A|\neg 0\le C\right\}⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
224	210 223	ax-mp	$$⊢{\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}=\left(x\in \left\{x\in A|\neg 0\le C\right\}⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)$$
225		resmpt	$$⊢\left\{x\in A|\neg 0\le C\right\}\subseteq A\to {\left(y\in A⟼⦋y/x⦌if\left(0\le B,B,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}=\left(y\in \left\{x\in A|\neg 0\le C\right\}⟼⦋y/x⦌if\left(0\le B,B,0\right)\right)$$
226		nfcv	$$⊢\underset{\_}{Ⅎ}yif\left(0\le B,B,0\right)$$
227		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌if\left(0\le B,B,0\right)$$
228		csbeq1a	$$⊢x=y\to if\left(0\le B,B,0\right)=⦋y/x⦌if\left(0\le B,B,0\right)$$
229	226 227 228	cbvmpt	$$⊢\left(x\in A⟼if\left(0\le B,B,0\right)\right)=\left(y\in A⟼⦋y/x⦌if\left(0\le B,B,0\right)\right)$$
230	229	reseq1i	$$⊢{\left(x\in A⟼if\left(0\le B,B,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}={\left(y\in A⟼⦋y/x⦌if\left(0\le B,B,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}$$
231		nfv	$$⊢Ⅎy\left(x\in \left\{x\in A|\neg 0\le C\right\}\wedge z=if\left(0\le B,B,0\right)\right)$$
232	227	nfeq2	$$⊢Ⅎxz=⦋y/x⦌if\left(0\le B,B,0\right)$$
233	215 232	nfan	$$⊢Ⅎx\left(y\in \left\{x\in A|\neg 0\le C\right\}\wedge z=⦋y/x⦌if\left(0\le B,B,0\right)\right)$$
234	228	eqeq2d	$$⊢x=y\to \left(z=if\left(0\le B,B,0\right)\leftrightarrow z=⦋y/x⦌if\left(0\le B,B,0\right)\right)$$
235	217 234	anbi12d	$$⊢x=y\to \left(\left(x\in \left\{x\in A|\neg 0\le C\right\}\wedge z=if\left(0\le B,B,0\right)\right)\leftrightarrow \left(y\in \left\{x\in A|\neg 0\le C\right\}\wedge z=⦋y/x⦌if\left(0\le B,B,0\right)\right)\right)$$
236	231 233 235	cbvopab1	$$⊢\left\{⟨x,z⟩|\left(x\in \left\{x\in A|\neg 0\le C\right\}\wedge z=if\left(0\le B,B,0\right)\right)\right\}=\left\{⟨y,z⟩|\left(y\in \left\{x\in A|\neg 0\le C\right\}\wedge z=⦋y/x⦌if\left(0\le B,B,0\right)\right)\right\}$$
237		df-mpt	$$⊢\left(x\in \left\{x\in A|\neg 0\le C\right\}⟼if\left(0\le B,B,0\right)\right)=\left\{⟨x,z⟩|\left(x\in \left\{x\in A|\neg 0\le C\right\}\wedge z=if\left(0\le B,B,0\right)\right)\right\}$$
238		df-mpt	$$⊢\left(y\in \left\{x\in A|\neg 0\le C\right\}⟼⦋y/x⦌if\left(0\le B,B,0\right)\right)=\left\{⟨y,z⟩|\left(y\in \left\{x\in A|\neg 0\le C\right\}\wedge z=⦋y/x⦌if\left(0\le B,B,0\right)\right)\right\}$$
239	236 237 238	3eqtr4i	$$⊢\left(x\in \left\{x\in A|\neg 0\le C\right\}⟼if\left(0\le B,B,0\right)\right)=\left(y\in \left\{x\in A|\neg 0\le C\right\}⟼⦋y/x⦌if\left(0\le B,B,0\right)\right)$$
240	225 230 239	3eqtr4g	$$⊢\left\{x\in A|\neg 0\le C\right\}\subseteq A\to {\left(x\in A⟼if\left(0\le B,B,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}=\left(x\in \left\{x\in A|\neg 0\le C\right\}⟼if\left(0\le B,B,0\right)\right)$$
241	210 240	ax-mp	$$⊢{\left(x\in A⟼if\left(0\le B,B,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}=\left(x\in \left\{x\in A|\neg 0\le C\right\}⟼if\left(0\le B,B,0\right)\right)$$
242	209 224 241	3eqtr4g	$$⊢\phi \to {\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}={\left(x\in A⟼if\left(0\le B,B,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}$$
243	2 1	mbfpos	$$⊢\phi \to \left(x\in A⟼if\left(0\le B,B,0\right)\right)\in MblFn$$
244	103	mptpreima	$$⊢{\left(x\in A⟼C\right)}^{-1}\left[\left(\mathrm{-\infty },0\right)\right]=\left\{x\in A|C\in \left(\mathrm{-\infty },0\right)\right\}$$
245		elioomnf	$$⊢0\in {ℝ}^{*}\to \left(C\in \left(\mathrm{-\infty },0\right)\leftrightarrow \left(C\in ℝ\wedge C<0\right)\right)$$
246	78 245	ax-mp	$$⊢C\in \left(\mathrm{-\infty },0\right)\leftrightarrow \left(C\in ℝ\wedge C<0\right)$$
247	4	biantrurd	$$⊢\left(\phi \wedge x\in A\right)\to \left(C<0\leftrightarrow \left(C\in ℝ\wedge C<0\right)\right)$$
248		ltnle	$$⊢\left(C\in ℝ\wedge 0\in ℝ\right)\to \left(C<0\leftrightarrow \neg 0\le C\right)$$
249	4 6 248	sylancl	$$⊢\left(\phi \wedge x\in A\right)\to \left(C<0\leftrightarrow \neg 0\le C\right)$$
250	247 249	bitr3d	$$⊢\left(\phi \wedge x\in A\right)\to \left(\left(C\in ℝ\wedge C<0\right)\leftrightarrow \neg 0\le C\right)$$
251	246 250	bitrid	$$⊢\left(\phi \wedge x\in A\right)\to \left(C\in \left(\mathrm{-\infty },0\right)\leftrightarrow \neg 0\le C\right)$$
252	251	rabbidva	$$⊢\phi \to \left\{x\in A|C\in \left(\mathrm{-\infty },0\right)\right\}=\left\{x\in A|\neg 0\le C\right\}$$
253	244 252	eqtrid	$$⊢\phi \to {\left(x\in A⟼C\right)}^{-1}\left[\left(\mathrm{-\infty },0\right)\right]=\left\{x\in A|\neg 0\le C\right\}$$
254		mbfima	$$⊢\left(\left(x\in A⟼C\right)\in MblFn\wedge \left(x\in A⟼C\right):A⟶ℝ\right)\to {\left(x\in A⟼C\right)}^{-1}\left[\left(\mathrm{-\infty },0\right)\right]\in \mathrm{dom}vol$$
255	3 107 254	syl2anc	$$⊢\phi \to {\left(x\in A⟼C\right)}^{-1}\left[\left(\mathrm{-\infty },0\right)\right]\in \mathrm{dom}vol$$
256	253 255	eqeltrrd	$$⊢\phi \to \left\{x\in A|\neg 0\le C\right\}\in \mathrm{dom}vol$$
257		mbfres	$$⊢\left(\left(x\in A⟼if\left(0\le B,B,0\right)\right)\in MblFn\wedge \left\{x\in A|\neg 0\le C\right\}\in \mathrm{dom}vol\right)\to {\left(x\in A⟼if\left(0\le B,B,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}\in MblFn$$
258	243 256 257	syl2anc	$$⊢\phi \to {\left(x\in A⟼if\left(0\le B,B,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}\in MblFn$$
259	242 258	eqeltrd	$$⊢\phi \to {\left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\upharpoonright }_{\left\{x\in A|\neg 0\le C\right\}}\in MblFn$$
260		rabxm	$$⊢A=\left\{x\in A|0\le C\right\}\cup \left\{x\in A|\neg 0\le C\right\}$$
261	260	eqcomi	$$⊢\left\{x\in A|0\le C\right\}\cup \left\{x\in A|\neg 0\le C\right\}=A$$
262	261	a1i	$$⊢\phi \to \left\{x\in A|0\le C\right\}\cup \left\{x\in A|\neg 0\le C\right\}=A$$
263	12 200 259 262	mbfres2	$$⊢\phi \to \left(x\in A⟼if\left(0\le B,B,0\right)+if\left(0\le C,C,0\right)\right)\in MblFn$$