Theorem mbfposadd 30224

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	|- ( ph -> ( x e. A |-> B ) e. MblFn )
mbfposadd.2	|- ( ( ph /\ x e. A ) -> B e. RR )
mbfposadd.3	|- ( ph -> ( x e. A |-> C ) e. MblFn )
mbfposadd.4	|- ( ( ph /\ x e. A ) -> C e. RR )
mbfposadd.5	|- ( ph -> ( x e. A |-> ( B + C ) ) e. MblFn )

Assertion

Ref	Expression
mbfposadd	|- ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) e. MblFn )

Distinct variable groups:   ph, x   x, A

Allowed substitution hints:   B( x)   C( x)

Proof of Theorem mbfposadd

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mbfposadd.2	. . . . 5 |- ( ( ph /\ x e. A ) -> B e. RR )
2		0re 9613	. . . . 5 |- 0 e. RR
3		ifcl 3986	. . . . 5 |- ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
4	1, 2, 3	sylancl 662	. . . 4 |- ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
5		mbfposadd.4	. . . . 5 |- ( ( ph /\ x e. A ) -> C e. RR )
6		ifcl 3986	. . . . 5 |- ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
7	5, 2, 6	sylancl 662	. . . 4 |- ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
8	4, 7	readdcld 9640	. . 3 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR )
9		eqid 2457	. . 3 |- ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
10	8, 9	fmptd 6056	. 2 |- ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) : A --> RR )
11		ssrab2 3581	. . . 4 |- { x e. A | 0 <_ C } C_ A
12		fssres 5757	. . . 4 |- ( ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) : A --> RR /\ { x e. A | 0 <_ C } C_ A ) -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) : { x e. A | 0 <_ C } --> RR )
13	10, 11, 12	sylancl 662	. . 3 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) : { x e. A | 0 <_ C } --> RR )
14		inss2 3715	. . . . . 6 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C }
15		resabs1 5312	. . . . . 6 |- ( ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C } -> ( ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) )
16	14, 15	ax-mp 5	. . . . 5 |- ( ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) )
17		elin 3683	. . . . . . . . 9 |- ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) <-> ( x e. { x e. A | 0 <_ B } /\ x e. { x e. A | 0 <_ C } ) )
18		rabid 3034	. . . . . . . . . 10 |- ( x e. { x e. A | 0 <_ B } <-> ( x e. A /\ 0 <_ B ) )
19		rabid 3034	. . . . . . . . . 10 |- ( x e. { x e. A | 0 <_ C } <-> ( x e. A /\ 0 <_ C ) )
20	18, 19	anbi12i 697	. . . . . . . . 9 |- ( ( x e. { x e. A | 0 <_ B } /\ x e. { x e. A | 0 <_ C } ) <-> ( ( x e. A /\ 0 <_ B ) /\ ( x e. A /\ 0 <_ C ) ) )
21	17, 20	bitri 249	. . . . . . . 8 |- ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) <-> ( ( x e. A /\ 0 <_ B ) /\ ( x e. A /\ 0 <_ C ) ) )
22		iftrue 3950	. . . . . . . . . 10 |- ( 0 <_ B -> if ( 0 <_ B , B , 0 ) = B )
23		iftrue 3950	. . . . . . . . . 10 |- ( 0 <_ C -> if ( 0 <_ C , C , 0 ) = C )
24	22, 23	oveqan12d 6315	. . . . . . . . 9 |- ( ( 0 <_ B /\ 0 <_ C ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( B + C ) )
25	24	ad2ant2l 745	. . . . . . . 8 |- ( ( ( x e. A /\ 0 <_ B ) /\ ( x e. A /\ 0 <_ C ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( B + C ) )
26	21, 25	sylbi 195	. . . . . . 7 |- ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( B + C ) )
27	26	mpteq2ia 4539	. . . . . 6 |- ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( B + C ) )
28		inss1 3714	. . . . . . . 8 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ B }
29		ssrab2 3581	. . . . . . . 8 |- { x e. A | 0 <_ B } C_ A
30	28, 29	sstri 3508	. . . . . . 7 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A
31		resmpt 5333	. . . . . . . 8 |- ( ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A -> ( ( y e. A |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
32		nfcv 2619	. . . . . . . . . 10 |- F/_ y ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
33		nfcsb1v 3446	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
34		csbeq1a 3439	. . . . . . . . . 10 |- ( x = y -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
35	32, 33, 34	cbvmpt 4547	. . . . . . . . 9 |- ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( y e. A |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
36	35	reseq1i 5279	. . . . . . . 8 |- ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( ( y e. A |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) )
37		nfv 1708	. . . . . . . . . 10 |- F/ y ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
38		nfrab1 3038	. . . . . . . . . . . . 13 |- F/_ x { x e. A | 0 <_ B }
39		nfrab1 3038	. . . . . . . . . . . . 13 |- F/_ x { x e. A | 0 <_ C }
40	38, 39	nfin 3701	. . . . . . . . . . . 12 |- F/_ x ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } )
41	40	nfcri 2612	. . . . . . . . . . 11 |- F/ x y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } )
42	33	nfeq2 2636	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
43	41, 42	nfan 1929	. . . . . . . . . 10 |- F/ x ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
44		eleq1 2529	. . . . . . . . . . 11 |- ( x = y -> ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) <-> y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) )
45	34	eqeq2d 2471	. . . . . . . . . . 11 |- ( x = y -> ( z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) <-> z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
46	44, 45	anbi12d 710	. . . . . . . . . 10 |- ( x = y -> ( ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) <-> ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) ) )
47	37, 43, 46	cbvopab1 4527	. . . . . . . . 9 |- { <. x , z >. | ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) } = { <. y , z >. | ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) }
48		df-mpt 4517	. . . . . . . . 9 |- ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = { <. x , z >. | ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) }
49		df-mpt 4517	. . . . . . . . 9 |- ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = { <. y , z >. | ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) }
50	47, 48, 49	3eqtr4i 2496	. . . . . . . 8 |- ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
51	31, 36, 50	3eqtr4g 2523	. . . . . . 7 |- ( ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
52	30, 51	ax-mp 5	. . . . . 6 |- ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
53		resmpt 5333	. . . . . . . 8 |- ( ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A -> ( ( y e. A |-> [_ y / x ]_ ( B + C ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> [_ y / x ]_ ( B + C ) ) )
54		nfcv 2619	. . . . . . . . . 10 |- F/_ y ( B + C )
55		nfcsb1v 3446	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ ( B + C )
56		csbeq1a 3439	. . . . . . . . . 10 |- ( x = y -> ( B + C ) = [_ y / x ]_ ( B + C ) )
57	54, 55, 56	cbvmpt 4547	. . . . . . . . 9 |- ( x e. A |-> ( B + C ) ) = ( y e. A |-> [_ y / x ]_ ( B + C ) )
58	57	reseq1i 5279	. . . . . . . 8 |- ( ( x e. A |-> ( B + C ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( ( y e. A |-> [_ y / x ]_ ( B + C ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) )
59		nfv 1708	. . . . . . . . . 10 |- F/ y ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( B + C ) )
60	55	nfeq2 2636	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ ( B + C )
61	41, 60	nfan 1929	. . . . . . . . . 10 |- F/ x ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( B + C ) )
62	56	eqeq2d 2471	. . . . . . . . . . 11 |- ( x = y -> ( z = ( B + C ) <-> z = [_ y / x ]_ ( B + C ) ) )
63	44, 62	anbi12d 710	. . . . . . . . . 10 |- ( x = y -> ( ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( B + C ) ) <-> ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( B + C ) ) ) )
64	59, 61, 63	cbvopab1 4527	. . . . . . . . 9 |- { <. x , z >. | ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( B + C ) ) } = { <. y , z >. | ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( B + C ) ) }
65		df-mpt 4517	. . . . . . . . 9 |- ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( B + C ) ) = { <. x , z >. | ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( B + C ) ) }
66		df-mpt 4517	. . . . . . . . 9 |- ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> [_ y / x ]_ ( B + C ) ) = { <. y , z >. | ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( B + C ) ) }
67	64, 65, 66	3eqtr4i 2496	. . . . . . . 8 |- ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( B + C ) ) = ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> [_ y / x ]_ ( B + C ) )
68	53, 58, 67	3eqtr4g 2523	. . . . . . 7 |- ( ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A -> ( ( x e. A |-> ( B + C ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( B + C ) ) )
69	30, 68	ax-mp 5	. . . . . 6 |- ( ( x e. A |-> ( B + C ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( B + C ) )
70	27, 52, 69	3eqtr4i 2496	. . . . 5 |- ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( ( x e. A |-> ( B + C ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) )
71	16, 70	eqtri 2486	. . . 4 |- ( ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( ( x e. A |-> ( B + C ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) )
72		mbfposadd.5	. . . . 5 |- ( ph -> ( x e. A |-> ( B + C ) ) e. MblFn )
73	1	biantrurd 508	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( 0 <_ B <-> ( B e. RR /\ 0 <_ B ) ) )
74		elrege0 11652	. . . . . . . . . 10 |- ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
75	73, 74	syl6bbr 263	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( 0 <_ B <-> B e. ( 0 [,) +oo ) ) )
76	75	rabbidva 3100	. . . . . . . 8 |- ( ph -> { x e. A | 0 <_ B } = { x e. A | B e. ( 0 [,) +oo ) } )
77		0xr 9657	. . . . . . . . . . 11 |- 0 e. RR*
78		pnfxr 11346	. . . . . . . . . . 11 |- +oo e. RR*
79		0ltpnf 11357	. . . . . . . . . . 11 |- 0 < +oo
80		snunioo 11671	. . . . . . . . . . 11 |- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 < +oo ) -> ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo ) )
81	77, 78, 79, 80	mp3an 1324	. . . . . . . . . 10 |- ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo )
82	81	imaeq2i 5345	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( x e. A |-> B ) " ( 0 [,) +oo ) )
83		imaundi 5425	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) )
84		eqid 2457	. . . . . . . . . 10 |- ( x e. A |-> B ) = ( x e. A |-> B )
85	84	mptpreima 5506	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( 0 [,) +oo ) ) = { x e. A | B e. ( 0 [,) +oo ) }
86	82, 83, 85	3eqtr3ri 2495	. . . . . . . 8 |- { x e. A | B e. ( 0 [,) +oo ) } = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) )
87	76, 86	syl6eq 2514	. . . . . . 7 |- ( ph -> { x e. A | 0 <_ B } = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) ) )
88		mbfposadd.1	. . . . . . . 8 |- ( ph -> ( x e. A |-> B ) e. MblFn )
89	1, 84	fmptd 6056	. . . . . . . 8 |- ( ph -> ( x e. A |-> B ) : A --> RR )
90		mbfimasn 22166	. . . . . . . . . 10 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR /\ 0 e. RR ) -> ( `' ( x e. A |-> B ) " { 0 } ) e. dom vol )
91	2, 90	mp3an3 1313	. . . . . . . . 9 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " { 0 } ) e. dom vol )
92		mbfima 22164	. . . . . . . . 9 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) e. dom vol )
93		unmbl 22073	. . . . . . . . 9 |- ( ( ( `' ( x e. A |-> B ) " { 0 } ) e. dom vol /\ ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) e. dom vol ) -> ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) ) e. dom vol )
94	91, 92, 93	syl2anc 661	. . . . . . . 8 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) ) e. dom vol )
95	88, 89, 94	syl2anc 661	. . . . . . 7 |- ( ph -> ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) ) e. dom vol )
96	87, 95	eqeltrd 2545	. . . . . 6 |- ( ph -> { x e. A | 0 <_ B } e. dom vol )
97	5	biantrurd 508	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( 0 <_ C <-> ( C e. RR /\ 0 <_ C ) ) )
98		elrege0 11652	. . . . . . . . . 10 |- ( C e. ( 0 [,) +oo ) <-> ( C e. RR /\ 0 <_ C ) )
99	97, 98	syl6bbr 263	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( 0 <_ C <-> C e. ( 0 [,) +oo ) ) )
100	99	rabbidva 3100	. . . . . . . 8 |- ( ph -> { x e. A | 0 <_ C } = { x e. A | C e. ( 0 [,) +oo ) } )
101	81	imaeq2i 5345	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( x e. A |-> C ) " ( 0 [,) +oo ) )
102		imaundi 5425	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) )
103		eqid 2457	. . . . . . . . . 10 |- ( x e. A |-> C ) = ( x e. A |-> C )
104	103	mptpreima 5506	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( 0 [,) +oo ) ) = { x e. A | C e. ( 0 [,) +oo ) }
105	101, 102, 104	3eqtr3ri 2495	. . . . . . . 8 |- { x e. A | C e. ( 0 [,) +oo ) } = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) )
106	100, 105	syl6eq 2514	. . . . . . 7 |- ( ph -> { x e. A | 0 <_ C } = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) ) )
107		mbfposadd.3	. . . . . . . 8 |- ( ph -> ( x e. A |-> C ) e. MblFn )
108	5, 103	fmptd 6056	. . . . . . . 8 |- ( ph -> ( x e. A |-> C ) : A --> RR )
109		mbfimasn 22166	. . . . . . . . . 10 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR /\ 0 e. RR ) -> ( `' ( x e. A |-> C ) " { 0 } ) e. dom vol )
110	2, 109	mp3an3 1313	. . . . . . . . 9 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " { 0 } ) e. dom vol )
111		mbfima 22164	. . . . . . . . 9 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) e. dom vol )
112		unmbl 22073	. . . . . . . . 9 |- ( ( ( `' ( x e. A |-> C ) " { 0 } ) e. dom vol /\ ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) e. dom vol ) -> ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) ) e. dom vol )
113	110, 111, 112	syl2anc 661	. . . . . . . 8 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) ) e. dom vol )
114	107, 108, 113	syl2anc 661	. . . . . . 7 |- ( ph -> ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) ) e. dom vol )
115	106, 114	eqeltrd 2545	. . . . . 6 |- ( ph -> { x e. A | 0 <_ C } e. dom vol )
116		inmbl 22077	. . . . . 6 |- ( ( { x e. A | 0 <_ B } e. dom vol /\ { x e. A | 0 <_ C } e. dom vol ) -> ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol )
117	96, 115, 116	syl2anc 661	. . . . 5 |- ( ph -> ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol )
118		mbfres 22176	. . . . 5 |- ( ( ( x e. A |-> ( B + C ) ) e. MblFn /\ ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol ) -> ( ( x e. A |-> ( B + C ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) e. MblFn )
119	72, 117, 118	syl2anc 661	. . . 4 |- ( ph -> ( ( x e. A |-> ( B + C ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) e. MblFn )
120	71, 119	syl5eqel 2549	. . 3 |- ( ph -> ( ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) e. MblFn )
121		inss2 3715	. . . . . 6 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C }
122		resabs1 5312	. . . . . 6 |- ( ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C } -> ( ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) )
123	121, 122	ax-mp 5	. . . . 5 |- ( ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) )
124		rabid 3034	. . . . . . . . . 10 |- ( x e. { x e. A | -. 0 <_ B } <-> ( x e. A /\ -. 0 <_ B ) )
125	124, 19	anbi12i 697	. . . . . . . . 9 |- ( ( x e. { x e. A | -. 0 <_ B } /\ x e. { x e. A | 0 <_ C } ) <-> ( ( x e. A /\ -. 0 <_ B ) /\ ( x e. A /\ 0 <_ C ) ) )
126		elin 3683	. . . . . . . . 9 |- ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) <-> ( x e. { x e. A | -. 0 <_ B } /\ x e. { x e. A | 0 <_ C } ) )
127		anandi 828	. . . . . . . . 9 |- ( ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) <-> ( ( x e. A /\ -. 0 <_ B ) /\ ( x e. A /\ 0 <_ C ) ) )
128	125, 126, 127	3bitr4i 277	. . . . . . . 8 |- ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) <-> ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) )
129		iffalse 3953	. . . . . . . . . . 11 |- ( -. 0 <_ B -> if ( 0 <_ B , B , 0 ) = 0 )
130	129, 23	oveqan12d 6315	. . . . . . . . . 10 |- ( ( -. 0 <_ B /\ 0 <_ C ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( 0 + C ) )
131	130	ad2antll 728	. . . . . . . . 9 |- ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( 0 + C ) )
132	5	recnd 9639	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> C e. CC )
133	132	addid2d 9798	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( 0 + C ) = C )
134	133	adantrr 716	. . . . . . . . 9 |- ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( 0 + C ) = C )
135	131, 134	eqtrd 2498	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = C )
136	128, 135	sylan2b 475	. . . . . . 7 |- ( ( ph /\ x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = C )
137	136	mpteq2dva 4543	. . . . . 6 |- ( ph -> ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> C ) )
138		inss1 3714	. . . . . . . 8 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | -. 0 <_ B }
139		ssrab2 3581	. . . . . . . 8 |- { x e. A | -. 0 <_ B } C_ A
140	138, 139	sstri 3508	. . . . . . 7 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A
141		resmpt 5333	. . . . . . . 8 |- ( ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A -> ( ( y e. A |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
142	35	reseq1i 5279	. . . . . . . 8 |- ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( ( y e. A |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) )
143		nfv 1708	. . . . . . . . . 10 |- F/ y ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
144		nfrab1 3038	. . . . . . . . . . . . 13 |- F/_ x { x e. A | -. 0 <_ B }
145	144, 39	nfin 3701	. . . . . . . . . . . 12 |- F/_ x ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } )
146	145	nfcri 2612	. . . . . . . . . . 11 |- F/ x y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } )
147	146, 42	nfan 1929	. . . . . . . . . 10 |- F/ x ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
148		eleq1 2529	. . . . . . . . . . 11 |- ( x = y -> ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) <-> y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) )
149	148, 45	anbi12d 710	. . . . . . . . . 10 |- ( x = y -> ( ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) <-> ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) ) )
150	143, 147, 149	cbvopab1 4527	. . . . . . . . 9 |- { <. x , z >. | ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) } = { <. y , z >. | ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) }
151		df-mpt 4517	. . . . . . . . 9 |- ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = { <. x , z >. | ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) }
152		df-mpt 4517	. . . . . . . . 9 |- ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = { <. y , z >. | ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) }
153	150, 151, 152	3eqtr4i 2496	. . . . . . . 8 |- ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
154	141, 142, 153	3eqtr4g 2523	. . . . . . 7 |- ( ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
155	140, 154	ax-mp 5	. . . . . 6 |- ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
156		resmpt 5333	. . . . . . . 8 |- ( ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A -> ( ( y e. A |-> [_ y / x ]_ C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> [_ y / x ]_ C ) )
157		nfcv 2619	. . . . . . . . . 10 |- F/_ y C
158		nfcsb1v 3446	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ C
159		csbeq1a 3439	. . . . . . . . . 10 |- ( x = y -> C = [_ y / x ]_ C )
160	157, 158, 159	cbvmpt 4547	. . . . . . . . 9 |- ( x e. A |-> C ) = ( y e. A |-> [_ y / x ]_ C )
161	160	reseq1i 5279	. . . . . . . 8 |- ( ( x e. A |-> C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( ( y e. A |-> [_ y / x ]_ C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) )
162		nfv 1708	. . . . . . . . . 10 |- F/ y ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = C )
163	158	nfeq2 2636	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ C
164	146, 163	nfan 1929	. . . . . . . . . 10 |- F/ x ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ C )
165	159	eqeq2d 2471	. . . . . . . . . . 11 |- ( x = y -> ( z = C <-> z = [_ y / x ]_ C ) )
166	148, 165	anbi12d 710	. . . . . . . . . 10 |- ( x = y -> ( ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = C ) <-> ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ C ) ) )
167	162, 164, 166	cbvopab1 4527	. . . . . . . . 9 |- { <. x , z >. | ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = C ) } = { <. y , z >. | ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ C ) }
168		df-mpt 4517	. . . . . . . . 9 |- ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> C ) = { <. x , z >. | ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = C ) }
169		df-mpt 4517	. . . . . . . . 9 |- ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> [_ y / x ]_ C ) = { <. y , z >. | ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ C ) }
170	167, 168, 169	3eqtr4i 2496	. . . . . . . 8 |- ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> C ) = ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> [_ y / x ]_ C )
171	156, 161, 170	3eqtr4g 2523	. . . . . . 7 |- ( ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A -> ( ( x e. A |-> C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> C ) )
172	140, 171	ax-mp 5	. . . . . 6 |- ( ( x e. A |-> C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) |-> C )
173	137, 155, 172	3eqtr4g 2523	. . . . 5 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( ( x e. A |-> C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) )
174	123, 173	syl5eq 2510	. . . 4 |- ( ph -> ( ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = ( ( x e. A |-> C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) )
175	84	mptpreima 5506	. . . . . . . 8 |- ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) = { x e. A | B e. ( -oo (,) 0 ) }
176		elioomnf 11644	. . . . . . . . . . 11 |- ( 0 e. RR* -> ( B e. ( -oo (,) 0 ) <-> ( B e. RR /\ B < 0 ) ) )
177	77, 176	ax-mp 5	. . . . . . . . . 10 |- ( B e. ( -oo (,) 0 ) <-> ( B e. RR /\ B < 0 ) )
178	1	biantrurd 508	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( B < 0 <-> ( B e. RR /\ B < 0 ) ) )
179		ltnle 9681	. . . . . . . . . . . 12 |- ( ( B e. RR /\ 0 e. RR ) -> ( B < 0 <-> -. 0 <_ B ) )
180	1, 2, 179	sylancl 662	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( B < 0 <-> -. 0 <_ B ) )
181	178, 180	bitr3d 255	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( ( B e. RR /\ B < 0 ) <-> -. 0 <_ B ) )
182	177, 181	syl5bb 257	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( B e. ( -oo (,) 0 ) <-> -. 0 <_ B ) )
183	182	rabbidva 3100	. . . . . . . 8 |- ( ph -> { x e. A | B e. ( -oo (,) 0 ) } = { x e. A | -. 0 <_ B } )
184	175, 183	syl5eq 2510	. . . . . . 7 |- ( ph -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) = { x e. A | -. 0 <_ B } )
185		mbfima 22164	. . . . . . . 8 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) e. dom vol )
186	88, 89, 185	syl2anc 661	. . . . . . 7 |- ( ph -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) e. dom vol )
187	184, 186	eqeltrrd 2546	. . . . . 6 |- ( ph -> { x e. A | -. 0 <_ B } e. dom vol )
188		inmbl 22077	. . . . . 6 |- ( ( { x e. A | -. 0 <_ B } e. dom vol /\ { x e. A | 0 <_ C } e. dom vol ) -> ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol )
189	187, 115, 188	syl2anc 661	. . . . 5 |- ( ph -> ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol )
190		mbfres 22176	. . . . 5 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol ) -> ( ( x e. A |-> C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) e. MblFn )
191	107, 189, 190	syl2anc 661	. . . 4 |- ( ph -> ( ( x e. A |-> C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) e. MblFn )
192	174, 191	eqeltrd 2545	. . 3 |- ( ph -> ( ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) e. MblFn )
193		ssid 3518	. . . . . 6 |- A C_ A
194		dfrab3ss 3783	. . . . . 6 |- ( A C_ A -> { x e. A | 0 <_ C } = ( A i^i { x e. A | 0 <_ C } ) )
195	193, 194	ax-mp 5	. . . . 5 |- { x e. A | 0 <_ C } = ( A i^i { x e. A | 0 <_ C } )
196		rabxm 3817	. . . . . 6 |- A = ( { x e. A | 0 <_ B } u. { x e. A | -. 0 <_ B } )
197	196	ineq1i 3692	. . . . 5 |- ( A i^i { x e. A | 0 <_ C } ) = ( ( { x e. A | 0 <_ B } u. { x e. A | -. 0 <_ B } ) i^i { x e. A | 0 <_ C } )
198		indir 3753	. . . . 5 |- ( ( { x e. A | 0 <_ B } u. { x e. A | -. 0 <_ B } ) i^i { x e. A | 0 <_ C } ) = ( ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) u. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) )
199	195, 197, 198	3eqtrri 2491	. . . 4 |- ( ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) u. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = { x e. A | 0 <_ C }
200	199	a1i 11	. . 3 |- ( ph -> ( ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) u. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) = { x e. A | 0 <_ C } )
201	13, 120, 192, 200	mbfres2 22177	. 2 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) e. MblFn )
202		rabid 3034	. . . . . 6 |- ( x e. { x e. A | -. 0 <_ C } <-> ( x e. A /\ -. 0 <_ C ) )
203		iffalse 3953	. . . . . . . . 9 |- ( -. 0 <_ C -> if ( 0 <_ C , C , 0 ) = 0 )
204	203	oveq2d 6312	. . . . . . . 8 |- ( -. 0 <_ C -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( if ( 0 <_ B , B , 0 ) + 0 ) )
205	4	recnd 9639	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. CC )
206	205	addid1d 9797	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + 0 ) = if ( 0 <_ B , B , 0 ) )
207	204, 206	sylan9eqr 2520	. . . . . . 7 |- ( ( ( ph /\ x e. A ) /\ -. 0 <_ C ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ B , B , 0 ) )
208	207	anasss 647	. . . . . 6 |- ( ( ph /\ ( x e. A /\ -. 0 <_ C ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ B , B , 0 ) )
209	202, 208	sylan2b 475	. . . . 5 |- ( ( ph /\ x e. { x e. A | -. 0 <_ C } ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ B , B , 0 ) )
210	209	mpteq2dva 4543	. . . 4 |- ( ph -> ( x e. { x e. A | -. 0 <_ C } |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( x e. { x e. A | -. 0 <_ C } |-> if ( 0 <_ B , B , 0 ) ) )
211		ssrab2 3581	. . . . 5 |- { x e. A | -. 0 <_ C } C_ A
212		resmpt 5333	. . . . . 6 |- ( { x e. A | -. 0 <_ C } C_ A -> ( ( y e. A |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | -. 0 <_ C } ) = ( y e. { x e. A | -. 0 <_ C } |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
213	35	reseq1i 5279	. . . . . 6 |- ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | -. 0 <_ C } ) = ( ( y e. A |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | -. 0 <_ C } )
214		nfv 1708	. . . . . . . 8 |- F/ y ( x e. { x e. A | -. 0 <_ C } /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
215		nfrab1 3038	. . . . . . . . . 10 |- F/_ x { x e. A | -. 0 <_ C }
216	215	nfcri 2612	. . . . . . . . 9 |- F/ x y e. { x e. A | -. 0 <_ C }
217	216, 42	nfan 1929	. . . . . . . 8 |- F/ x ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
218		eleq1 2529	. . . . . . . . 9 |- ( x = y -> ( x e. { x e. A | -. 0 <_ C } <-> y e. { x e. A | -. 0 <_ C } ) )
219	218, 45	anbi12d 710	. . . . . . . 8 |- ( x = y -> ( ( x e. { x e. A | -. 0 <_ C } /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) <-> ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) ) )
220	214, 217, 219	cbvopab1 4527	. . . . . . 7 |- { <. x , z >. | ( x e. { x e. A | -. 0 <_ C } /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) } = { <. y , z >. | ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) }
221		df-mpt 4517	. . . . . . 7 |- ( x e. { x e. A | -. 0 <_ C } |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = { <. x , z >. | ( x e. { x e. A | -. 0 <_ C } /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) }
222		df-mpt 4517	. . . . . . 7 |- ( y e. { x e. A | -. 0 <_ C } |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = { <. y , z >. | ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) }
223	220, 221, 222	3eqtr4i 2496	. . . . . 6 |- ( x e. { x e. A | -. 0 <_ C } |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( y e. { x e. A | -. 0 <_ C } |-> [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
224	212, 213, 223	3eqtr4g 2523	. . . . 5 |- ( { x e. A | -. 0 <_ C } C_ A -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | -. 0 <_ C } ) = ( x e. { x e. A | -. 0 <_ C } |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) )
225	211, 224	ax-mp 5	. . . 4 |- ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | -. 0 <_ C } ) = ( x e. { x e. A | -. 0 <_ C } |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
226		resmpt 5333	. . . . . 6 |- ( { x e. A | -. 0 <_ C } C_ A -> ( ( y e. A |-> [_ y / x ]_ if ( 0 <_ B , B , 0 ) ) |` { x e. A | -. 0 <_ C } ) = ( y e. { x e. A | -. 0 <_ C } |-> [_ y / x ]_ if ( 0 <_ B , B , 0 ) ) )
227		nfcv 2619	. . . . . . . 8 |- F/_ y if ( 0 <_ B , B , 0 )
228		nfcsb1v 3446	. . . . . . . 8 |- F/_ x [_ y / x ]_ if ( 0 <_ B , B , 0 )
229		csbeq1a 3439	. . . . . . . 8 |- ( x = y -> if ( 0 <_ B , B , 0 ) = [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
230	227, 228, 229	cbvmpt 4547	. . . . . . 7 |- ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( y e. A |-> [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
231	230	reseq1i 5279	. . . . . 6 |- ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) |` { x e. A | -. 0 <_ C } ) = ( ( y e. A |-> [_ y / x ]_ if ( 0 <_ B , B , 0 ) ) |` { x e. A | -. 0 <_ C } )
232		nfv 1708	. . . . . . . 8 |- F/ y ( x e. { x e. A | -. 0 <_ C } /\ z = if ( 0 <_ B , B , 0 ) )
233	228	nfeq2 2636	. . . . . . . . 9 |- F/ x z = [_ y / x ]_ if ( 0 <_ B , B , 0 )
234	216, 233	nfan 1929	. . . . . . . 8 |- F/ x ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
235	229	eqeq2d 2471	. . . . . . . . 9 |- ( x = y -> ( z = if ( 0 <_ B , B , 0 ) <-> z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) ) )
236	218, 235	anbi12d 710	. . . . . . . 8 |- ( x = y -> ( ( x e. { x e. A | -. 0 <_ C } /\ z = if ( 0 <_ B , B , 0 ) ) <-> ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) ) ) )
237	232, 234, 236	cbvopab1 4527	. . . . . . 7 |- { <. x , z >. | ( x e. { x e. A | -. 0 <_ C } /\ z = if ( 0 <_ B , B , 0 ) ) } = { <. y , z >. | ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) ) }
238		df-mpt 4517	. . . . . . 7 |- ( x e. { x e. A | -. 0 <_ C } |-> if ( 0 <_ B , B , 0 ) ) = { <. x , z >. | ( x e. { x e. A | -. 0 <_ C } /\ z = if ( 0 <_ B , B , 0 ) ) }
239		df-mpt 4517	. . . . . . 7 |- ( y e. { x e. A | -. 0 <_ C } |-> [_ y / x ]_ if ( 0 <_ B , B , 0 ) ) = { <. y , z >. | ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) ) }
240	237, 238, 239	3eqtr4i 2496	. . . . . 6 |- ( x e. { x e. A | -. 0 <_ C } |-> if ( 0 <_ B , B , 0 ) ) = ( y e. { x e. A | -. 0 <_ C } |-> [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
241	226, 231, 240	3eqtr4g 2523	. . . . 5 |- ( { x e. A | -. 0 <_ C } C_ A -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) |` { x e. A | -. 0 <_ C } ) = ( x e. { x e. A | -. 0 <_ C } |-> if ( 0 <_ B , B , 0 ) ) )
242	211, 241	ax-mp 5	. . . 4 |- ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) |` { x e. A | -. 0 <_ C } ) = ( x e. { x e. A | -. 0 <_ C } |-> if ( 0 <_ B , B , 0 ) )
243	210, 225, 242	3eqtr4g 2523	. . 3 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | -. 0 <_ C } ) = ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) |` { x e. A | -. 0 <_ C } ) )
244	1, 88	mbfpos 22183	. . . 4 |- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
245	103	mptpreima 5506	. . . . . 6 |- ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) = { x e. A | C e. ( -oo (,) 0 ) }
246		elioomnf 11644	. . . . . . . . 9 |- ( 0 e. RR* -> ( C e. ( -oo (,) 0 ) <-> ( C e. RR /\ C < 0 ) ) )
247	77, 246	ax-mp 5	. . . . . . . 8 |- ( C e. ( -oo (,) 0 ) <-> ( C e. RR /\ C < 0 ) )
248	5	biantrurd 508	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( C < 0 <-> ( C e. RR /\ C < 0 ) ) )
249		ltnle 9681	. . . . . . . . . 10 |- ( ( C e. RR /\ 0 e. RR ) -> ( C < 0 <-> -. 0 <_ C ) )
250	5, 2, 249	sylancl 662	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( C < 0 <-> -. 0 <_ C ) )
251	248, 250	bitr3d 255	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( ( C e. RR /\ C < 0 ) <-> -. 0 <_ C ) )
252	247, 251	syl5bb 257	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( C e. ( -oo (,) 0 ) <-> -. 0 <_ C ) )
253	252	rabbidva 3100	. . . . . 6 |- ( ph -> { x e. A | C e. ( -oo (,) 0 ) } = { x e. A | -. 0 <_ C } )
254	245, 253	syl5eq 2510	. . . . 5 |- ( ph -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) = { x e. A | -. 0 <_ C } )
255		mbfima 22164	. . . . . 6 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) e. dom vol )
256	107, 108, 255	syl2anc 661	. . . . 5 |- ( ph -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) e. dom vol )
257	254, 256	eqeltrrd 2546	. . . 4 |- ( ph -> { x e. A | -. 0 <_ C } e. dom vol )
258		mbfres 22176	. . . 4 |- ( ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ { x e. A | -. 0 <_ C } e. dom vol ) -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) |` { x e. A | -. 0 <_ C } ) e. MblFn )
259	244, 257, 258	syl2anc 661	. . 3 |- ( ph -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) |` { x e. A | -. 0 <_ C } ) e. MblFn )
260	243, 259	eqeltrd 2545	. 2 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | -. 0 <_ C } ) e. MblFn )
261		rabxm 3817	. . . 4 |- A = ( { x e. A | 0 <_ C } u. { x e. A | -. 0 <_ C } )
262	261	eqcomi 2470	. . 3 |- ( { x e. A | 0 <_ C } u. { x e. A | -. 0 <_ C } ) = A
263	262	a1i 11	. 2 |- ( ph -> ( { x e. A | 0 <_ C } u. { x e. A | -. 0 <_ C } ) = A )
264	10, 201, 260, 263	mbfres2 22177	1 |- ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) e. MblFn )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1395   e. wcel 1819   {crab 2811   [_csb 3430   u. cun 3469   i^i cin 3470   C_ wss 3471   ifcif 3944   {csn 4032   class class class wbr 4456   {copab 4514   |-> cmpt 4515   `'ccnv 5007   dom cdm 5008   |` cres 5010   "cima 5011   -->wf 5590  (class class class)co 6296   RRcr 9508   0cc0 9509   + caddc 9512   +oocpnf 9642   -oocmnf 9643   RR*cxr 9644   < clt 9645   <_ cle 9646   (,)cioo 11554   [,)cico 11556   volcvol 22000  MblFncmbf 22148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-inf2 8075  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586  ax-pre-sup 9587

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-se 4848  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6539  df-om 6700  df-1st 6799  df-2nd 6800  df-recs 7060  df-rdg 7094  df-1o 7148  df-2o 7149  df-oadd 7152  df-er 7329  df-map 7440  df-pm 7441  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-sup 7919  df-oi 7953  df-card 8337  df-cda 8565  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-div 10228  df-nn 10557  df-2 10615  df-3 10616  df-n0 10817  df-z 10886  df-uz 11107  df-q 11208  df-rp 11246  df-xadd 11344  df-ioo 11558  df-ico 11560  df-icc 11561  df-fz 11698  df-fzo 11821  df-fl 11931  df-seq 12110  df-exp 12169  df-hash 12408  df-cj 12943  df-re 12944  df-im 12945  df-sqrt 13079  df-abs 13080  df-clim 13322  df-sum 13520  df-xmet 18538  df-met 18539  df-ovol 22001  df-vol 22002  df-mbf 22153

This theorem is referenced by:  itgaddnclem2  30236