Theorem mbfposadd 31414

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 9625	. . . . 5 |- 0 e. RR
3		ifcl 3926	. . . . 5 |- ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
4	1, 2, 3	sylancl 660	. . . 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 3926	. . . . 5 |- ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
7	5, 2, 6	sylancl 660	. . . 4 |- ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
8	4, 7	readdcld 9652	. . 3 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR )
9		eqid 2402	. . 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 6032	. 2 |- ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) : A --> RR )
11		ssrab2 3523	. . . 4 |- { x e. A | 0 <_ C } C_ A
12		fssres 5733	. . . 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 660	. . 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 3659	. . . . . 6 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C }
15		resabs1 5121	. . . . . 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 3625	. . . . . . . . 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 2983	. . . . . . . . . 10 |- ( x e. { x e. A | 0 <_ B } <-> ( x e. A /\ 0 <_ B ) )
19		rabid 2983	. . . . . . . . . 10 |- ( x e. { x e. A | 0 <_ C } <-> ( x e. A /\ 0 <_ C ) )
20	18, 19	anbi12i 695	. . . . . . . . 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 3890	. . . . . . . . . 10 |- ( 0 <_ B -> if ( 0 <_ B , B , 0 ) = B )
23		iftrue 3890	. . . . . . . . . 10 |- ( 0 <_ C -> if ( 0 <_ C , C , 0 ) = C )
24	22, 23	oveqan12d 6296	. . . . . . . . 9 |- ( ( 0 <_ B /\ 0 <_ C ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( B + C ) )
25	24	ad2ant2l 744	. . . . . . . 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 4476	. . . . . 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 3658	. . . . . . . 8 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ B }
29		ssrab2 3523	. . . . . . . 8 |- { x e. A | 0 <_ B } C_ A
30	28, 29	sstri 3450	. . . . . . 7 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A
31		resmpt 5142	. . . . . . . 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 2564	. . . . . . . . . 10 |- F/_ y ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
33		nfcsb1v 3388	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
34		csbeq1a 3381	. . . . . . . . . 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 4485	. . . . . . . . 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 5089	. . . . . . . 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 1728	. . . . . . . . . 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 2987	. . . . . . . . . . . . 13 |- F/_ x { x e. A | 0 <_ B }
39		nfrab1 2987	. . . . . . . . . . . . 13 |- F/_ x { x e. A | 0 <_ C }
40	38, 39	nfin 3645	. . . . . . . . . . . 12 |- F/_ x ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } )
41	40	nfcri 2557	. . . . . . . . . . 11 |- F/ x y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } )
42	33	nfeq2 2581	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
43	41, 42	nfan 1956	. . . . . . . . . 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 2474	. . . . . . . . . . 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 2416	. . . . . . . . . . 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 709	. . . . . . . . . 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 4464	. . . . . . . . 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 4454	. . . . . . . . 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 4454	. . . . . . . . 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 2441	. . . . . . . 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 2468	. . . . . . 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 5142	. . . . . . . 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 2564	. . . . . . . . . 10 |- F/_ y ( B + C )
55		nfcsb1v 3388	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ ( B + C )
56		csbeq1a 3381	. . . . . . . . . 10 |- ( x = y -> ( B + C ) = [_ y / x ]_ ( B + C ) )
57	54, 55, 56	cbvmpt 4485	. . . . . . . . 9 |- ( x e. A |-> ( B + C ) ) = ( y e. A |-> [_ y / x ]_ ( B + C ) )
58	57	reseq1i 5089	. . . . . . . 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 1728	. . . . . . . . . 10 |- F/ y ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( B + C ) )
60	55	nfeq2 2581	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ ( B + C )
61	41, 60	nfan 1956	. . . . . . . . . 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 2416	. . . . . . . . . . 11 |- ( x = y -> ( z = ( B + C ) <-> z = [_ y / x ]_ ( B + C ) ) )
63	44, 62	anbi12d 709	. . . . . . . . . 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 4464	. . . . . . . . 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 4454	. . . . . . . . 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 4454	. . . . . . . . 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 2441	. . . . . . . 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 2468	. . . . . . 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 2441	. . . . 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 2431	. . . 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 506	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( 0 <_ B <-> ( B e. RR /\ 0 <_ B ) ) )
74		elrege0 11679	. . . . . . . . . 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 3049	. . . . . . . 8 |- ( ph -> { x e. A | 0 <_ B } = { x e. A | B e. ( 0 [,) +oo ) } )
77		0xr 9669	. . . . . . . . . . 11 |- 0 e. RR*
78		pnfxr 11373	. . . . . . . . . . 11 |- +oo e. RR*
79		0ltpnf 11384	. . . . . . . . . . 11 |- 0 < +oo
80		snunioo 11698	. . . . . . . . . . 11 |- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 < +oo ) -> ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo ) )
81	77, 78, 79, 80	mp3an 1326	. . . . . . . . . 10 |- ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo )
82	81	imaeq2i 5154	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( x e. A |-> B ) " ( 0 [,) +oo ) )
83		imaundi 5235	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) )
84		eqid 2402	. . . . . . . . . 10 |- ( x e. A |-> B ) = ( x e. A |-> B )
85	84	mptpreima 5315	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( 0 [,) +oo ) ) = { x e. A | B e. ( 0 [,) +oo ) }
86	82, 83, 85	3eqtr3ri 2440	. . . . . . . 8 |- { x e. A | B e. ( 0 [,) +oo ) } = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) )
87	76, 86	syl6eq 2459	. . . . . . 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 6032	. . . . . . . 8 |- ( ph -> ( x e. A |-> B ) : A --> RR )
90		mbfimasn 22331	. . . . . . . . . 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 1315	. . . . . . . . 9 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " { 0 } ) e. dom vol )
92		mbfima 22329	. . . . . . . . 9 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) e. dom vol )
93		unmbl 22238	. . . . . . . . 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 659	. . . . . . . 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 659	. . . . . . 7 |- ( ph -> ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) ) e. dom vol )
96	87, 95	eqeltrd 2490	. . . . . 6 |- ( ph -> { x e. A | 0 <_ B } e. dom vol )
97	5	biantrurd 506	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( 0 <_ C <-> ( C e. RR /\ 0 <_ C ) ) )
98		elrege0 11679	. . . . . . . . . 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 3049	. . . . . . . 8 |- ( ph -> { x e. A | 0 <_ C } = { x e. A | C e. ( 0 [,) +oo ) } )
101	81	imaeq2i 5154	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( x e. A |-> C ) " ( 0 [,) +oo ) )
102		imaundi 5235	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) )
103		eqid 2402	. . . . . . . . . 10 |- ( x e. A |-> C ) = ( x e. A |-> C )
104	103	mptpreima 5315	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( 0 [,) +oo ) ) = { x e. A | C e. ( 0 [,) +oo ) }
105	101, 102, 104	3eqtr3ri 2440	. . . . . . . 8 |- { x e. A | C e. ( 0 [,) +oo ) } = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) )
106	100, 105	syl6eq 2459	. . . . . . 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 6032	. . . . . . . 8 |- ( ph -> ( x e. A |-> C ) : A --> RR )
109		mbfimasn 22331	. . . . . . . . . 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 1315	. . . . . . . . 9 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " { 0 } ) e. dom vol )
111		mbfima 22329	. . . . . . . . 9 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) e. dom vol )
112		unmbl 22238	. . . . . . . . 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 659	. . . . . . . 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 659	. . . . . . 7 |- ( ph -> ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) ) e. dom vol )
115	106, 114	eqeltrd 2490	. . . . . 6 |- ( ph -> { x e. A | 0 <_ C } e. dom vol )
116		inmbl 22242	. . . . . 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 659	. . . . 5 |- ( ph -> ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol )
118		mbfres 22341	. . . . 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 659	. . . 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 2494	. . 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 3659	. . . . . 6 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C }
122		resabs1 5121	. . . . . 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 2983	. . . . . . . . . 10 |- ( x e. { x e. A | -. 0 <_ B } <-> ( x e. A /\ -. 0 <_ B ) )
125	124, 19	anbi12i 695	. . . . . . . . 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 3625	. . . . . . . . 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 829	. . . . . . . . 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 3893	. . . . . . . . . . 11 |- ( -. 0 <_ B -> if ( 0 <_ B , B , 0 ) = 0 )
130	129, 23	oveqan12d 6296	. . . . . . . . . 10 |- ( ( -. 0 <_ B /\ 0 <_ C ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( 0 + C ) )
131	130	ad2antll 727	. . . . . . . . 9 |- ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( 0 + C ) )
132	5	recnd 9651	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> C e. CC )
133	132	addid2d 9814	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( 0 + C ) = C )
134	133	adantrr 715	. . . . . . . . 9 |- ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( 0 + C ) = C )
135	131, 134	eqtrd 2443	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = C )
136	128, 135	sylan2b 473	. . . . . . 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 4480	. . . . . 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 3658	. . . . . . . 8 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | -. 0 <_ B }
139		ssrab2 3523	. . . . . . . 8 |- { x e. A | -. 0 <_ B } C_ A
140	138, 139	sstri 3450	. . . . . . 7 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A
141		resmpt 5142	. . . . . . . 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 5089	. . . . . . . 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 1728	. . . . . . . . . 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 2987	. . . . . . . . . . . . 13 |- F/_ x { x e. A | -. 0 <_ B }
145	144, 39	nfin 3645	. . . . . . . . . . . 12 |- F/_ x ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } )
146	145	nfcri 2557	. . . . . . . . . . 11 |- F/ x y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } )
147	146, 42	nfan 1956	. . . . . . . . . 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 2474	. . . . . . . . . . 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 709	. . . . . . . . . 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 4464	. . . . . . . . 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 4454	. . . . . . . . 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 4454	. . . . . . . . 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 2441	. . . . . . . 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 2468	. . . . . . 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 5142	. . . . . . . 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 2564	. . . . . . . . . 10 |- F/_ y C
158		nfcsb1v 3388	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ C
159		csbeq1a 3381	. . . . . . . . . 10 |- ( x = y -> C = [_ y / x ]_ C )
160	157, 158, 159	cbvmpt 4485	. . . . . . . . 9 |- ( x e. A |-> C ) = ( y e. A |-> [_ y / x ]_ C )
161	160	reseq1i 5089	. . . . . . . 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 1728	. . . . . . . . . 10 |- F/ y ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = C )
163	158	nfeq2 2581	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ C
164	146, 163	nfan 1956	. . . . . . . . . 10 |- F/ x ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ C )
165	159	eqeq2d 2416	. . . . . . . . . . 11 |- ( x = y -> ( z = C <-> z = [_ y / x ]_ C ) )
166	148, 165	anbi12d 709	. . . . . . . . . 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 4464	. . . . . . . . 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 4454	. . . . . . . . 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 4454	. . . . . . . . 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 2441	. . . . . . . 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 2468	. . . . . . 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 2468	. . . . 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 2455	. . . 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 5315	. . . . . . . 8 |- ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) = { x e. A | B e. ( -oo (,) 0 ) }
176		elioomnf 11671	. . . . . . . . . . 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 506	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( B < 0 <-> ( B e. RR /\ B < 0 ) ) )
179		ltnle 9694	. . . . . . . . . . . 12 |- ( ( B e. RR /\ 0 e. RR ) -> ( B < 0 <-> -. 0 <_ B ) )
180	1, 2, 179	sylancl 660	. . . . . . . . . . 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 3049	. . . . . . . 8 |- ( ph -> { x e. A | B e. ( -oo (,) 0 ) } = { x e. A | -. 0 <_ B } )
184	175, 183	syl5eq 2455	. . . . . . 7 |- ( ph -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) = { x e. A | -. 0 <_ B } )
185		mbfima 22329	. . . . . . . 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 659	. . . . . . 7 |- ( ph -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) e. dom vol )
187	184, 186	eqeltrrd 2491	. . . . . 6 |- ( ph -> { x e. A | -. 0 <_ B } e. dom vol )
188		inmbl 22242	. . . . . 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 659	. . . . 5 |- ( ph -> ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol )
190		mbfres 22341	. . . . 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 659	. . . 4 |- ( ph -> ( ( x e. A |-> C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) e. MblFn )
192	174, 191	eqeltrd 2490	. . 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 3460	. . . . . 6 |- A C_ A
194		dfrab3ss 3727	. . . . . 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 3761	. . . . . 6 |- A = ( { x e. A | 0 <_ B } u. { x e. A | -. 0 <_ B } )
197	196	ineq1i 3636	. . . . 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 3697	. . . . 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 2436	. . . 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 22342	. 2 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) e. MblFn )
202		rabid 2983	. . . . . 6 |- ( x e. { x e. A | -. 0 <_ C } <-> ( x e. A /\ -. 0 <_ C ) )
203		iffalse 3893	. . . . . . . . 9 |- ( -. 0 <_ C -> if ( 0 <_ C , C , 0 ) = 0 )
204	203	oveq2d 6293	. . . . . . . 8 |- ( -. 0 <_ C -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( if ( 0 <_ B , B , 0 ) + 0 ) )
205	4	recnd 9651	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. CC )
206	205	addid1d 9813	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + 0 ) = if ( 0 <_ B , B , 0 ) )
207	204, 206	sylan9eqr 2465	. . . . . . 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 645	. . . . . 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 473	. . . . 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 4480	. . . 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 3523	. . . . 5 |- { x e. A | -. 0 <_ C } C_ A
212		resmpt 5142	. . . . . 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 5089	. . . . . 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 1728	. . . . . . . 8 |- F/ y ( x e. { x e. A | -. 0 <_ C } /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
215		nfrab1 2987	. . . . . . . . . 10 |- F/_ x { x e. A | -. 0 <_ C }
216	215	nfcri 2557	. . . . . . . . 9 |- F/ x y e. { x e. A | -. 0 <_ C }
217	216, 42	nfan 1956	. . . . . . . 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 2474	. . . . . . . . 9 |- ( x = y -> ( x e. { x e. A | -. 0 <_ C } <-> y e. { x e. A | -. 0 <_ C } ) )
219	218, 45	anbi12d 709	. . . . . . . 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 4464	. . . . . . 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 4454	. . . . . . 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 4454	. . . . . . 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 2441	. . . . . 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 2468	. . . . 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 5142	. . . . . 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 2564	. . . . . . . 8 |- F/_ y if ( 0 <_ B , B , 0 )
228		nfcsb1v 3388	. . . . . . . 8 |- F/_ x [_ y / x ]_ if ( 0 <_ B , B , 0 )
229		csbeq1a 3381	. . . . . . . 8 |- ( x = y -> if ( 0 <_ B , B , 0 ) = [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
230	227, 228, 229	cbvmpt 4485	. . . . . . 7 |- ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( y e. A |-> [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
231	230	reseq1i 5089	. . . . . 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 1728	. . . . . . . 8 |- F/ y ( x e. { x e. A | -. 0 <_ C } /\ z = if ( 0 <_ B , B , 0 ) )
233	228	nfeq2 2581	. . . . . . . . 9 |- F/ x z = [_ y / x ]_ if ( 0 <_ B , B , 0 )
234	216, 233	nfan 1956	. . . . . . . 8 |- F/ x ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
235	229	eqeq2d 2416	. . . . . . . . 9 |- ( x = y -> ( z = if ( 0 <_ B , B , 0 ) <-> z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) ) )
236	218, 235	anbi12d 709	. . . . . . . 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 4464	. . . . . . 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 4454	. . . . . . 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 4454	. . . . . . 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 2441	. . . . . 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 2468	. . . . 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 2468	. . 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 22348	. . . 4 |- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
245	103	mptpreima 5315	. . . . . 6 |- ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) = { x e. A | C e. ( -oo (,) 0 ) }
246		elioomnf 11671	. . . . . . . . 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 506	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( C < 0 <-> ( C e. RR /\ C < 0 ) ) )
249		ltnle 9694	. . . . . . . . . 10 |- ( ( C e. RR /\ 0 e. RR ) -> ( C < 0 <-> -. 0 <_ C ) )
250	5, 2, 249	sylancl 660	. . . . . . . . 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 3049	. . . . . 6 |- ( ph -> { x e. A | C e. ( -oo (,) 0 ) } = { x e. A | -. 0 <_ C } )
254	245, 253	syl5eq 2455	. . . . 5 |- ( ph -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) = { x e. A | -. 0 <_ C } )
255		mbfima 22329	. . . . . 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 659	. . . . 5 |- ( ph -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) e. dom vol )
257	254, 256	eqeltrrd 2491	. . . 4 |- ( ph -> { x e. A | -. 0 <_ C } e. dom vol )
258		mbfres 22341	. . . 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 659	. . 3 |- ( ph -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) |` { x e. A | -. 0 <_ C } ) e. MblFn )
260	243, 259	eqeltrd 2490	. 2 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | -. 0 <_ C } ) e. MblFn )
261		rabxm 3761	. . . 4 |- A = ( { x e. A | 0 <_ C } u. { x e. A | -. 0 <_ C } )
262	261	eqcomi 2415	. . 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 22342	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 367   = wceq 1405   e. wcel 1842   {crab 2757   [_csb 3372   u. cun 3411   i^i cin 3412   C_ wss 3413   ifcif 3884   {csn 3971   class class class wbr 4394   {copab 4451   |-> cmpt 4452   `'ccnv 4821   dom cdm 4822   |` cres 4824   "cima 4825   -->wf 5564  (class class class)co 6277   RRcr 9520   0cc0 9521   + caddc 9524   +oocpnf 9654   -oocmnf 9655   RR*cxr 9656   < clt 9657   <_ cle 9658   (,)cioo 11581   [,)cico 11583   volcvol 22165  MblFncmbf 22313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-inf2 8090  ax-cnex 9577  ax-resscn 9578  ax-1cn 9579  ax-icn 9580  ax-addcl 9581  ax-addrcl 9582  ax-mulcl 9583  ax-mulrcl 9584  ax-mulcom 9585  ax-addass 9586  ax-mulass 9587  ax-distr 9588  ax-i2m1 9589  ax-1ne0 9590  ax-1rid 9591  ax-rnegex 9592  ax-rrecex 9593  ax-cnre 9594  ax-pre-lttri 9595  ax-pre-lttrn 9596  ax-pre-ltadd 9597  ax-pre-mulgt0 9598  ax-pre-sup 9599

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-se 4782  df-we 4783  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-pred 5366  df-ord 5412  df-on 5413  df-lim 5414  df-suc 5415  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-isom 5577  df-riota 6239  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-of 6520  df-om 6683  df-1st 6783  df-2nd 6784  df-wrecs 7012  df-recs 7074  df-rdg 7112  df-1o 7166  df-2o 7167  df-oadd 7170  df-er 7347  df-map 7458  df-pm 7459  df-en 7554  df-dom 7555  df-sdom 7556  df-fin 7557  df-sup 7934  df-oi 7968  df-card 8351  df-cda 8579  df-pnf 9659  df-mnf 9660  df-xr 9661  df-ltxr 9662  df-le 9663  df-sub 9842  df-neg 9843  df-div 10247  df-nn 10576  df-2 10634  df-3 10635  df-n0 10836  df-z 10905  df-uz 11127  df-q 11227  df-rp 11265  df-xadd 11371  df-ioo 11585  df-ico 11587  df-icc 11588  df-fz 11725  df-fzo 11853  df-fl 11964  df-seq 12150  df-exp 12209  df-hash 12451  df-cj 13079  df-re 13080  df-im 13081  df-sqrt 13215  df-abs 13216  df-clim 13458  df-sum 13656  df-xmet 18730  df-met 18731  df-ovol 22166  df-vol 22167  df-mbf 22318

This theorem is referenced by:  itgaddnclem2  31427