Theorem mbfposadd 33457

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 10040	. . . . 5 |- 0 e. RR
3		ifcl 4130	. . . . 5 |- ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
4	1, 2, 3	sylancl 694	. . . 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 4130	. . . . 5 |- ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
7	5, 2, 6	sylancl 694	. . . 4 |- ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
8	4, 7	readdcld 10069	. . 3 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR )
9		eqid 2622	. . 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 6385	. 2 |- ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) : A --> RR )
11		ssrab2 3687	. . . 4 |- { x e. A | 0 <_ C } C_ A
12		fssres 6070	. . . 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 694	. . 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 3834	. . . . . 6 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C }
15		resabs1 5427	. . . . . 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 3796	. . . . . . . . 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 3116	. . . . . . . . . 10 |- ( x e. { x e. A | 0 <_ B } <-> ( x e. A /\ 0 <_ B ) )
19		rabid 3116	. . . . . . . . . 10 |- ( x e. { x e. A | 0 <_ C } <-> ( x e. A /\ 0 <_ C ) )
20	18, 19	anbi12i 733	. . . . . . . . 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 264	. . . . . . . 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 4092	. . . . . . . . . 10 |- ( 0 <_ B -> if ( 0 <_ B , B , 0 ) = B )
23		iftrue 4092	. . . . . . . . . 10 |- ( 0 <_ C -> if ( 0 <_ C , C , 0 ) = C )
24	22, 23	oveqan12d 6669	. . . . . . . . 9 |- ( ( 0 <_ B /\ 0 <_ C ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( B + C ) )
25	24	ad2ant2l 782	. . . . . . . 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 207	. . . . . . 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 4740	. . . . . 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 3833	. . . . . . . 8 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ B }
29		ssrab2 3687	. . . . . . . 8 |- { x e. A | 0 <_ B } C_ A
30	28, 29	sstri 3612	. . . . . . 7 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A
31		resmpt 5449	. . . . . . . 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 2764	. . . . . . . . . 10 |- F/_ y ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
33		nfcsb1v 3549	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
34		csbeq1a 3542	. . . . . . . . . 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 4749	. . . . . . . . 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 5392	. . . . . . . 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 1843	. . . . . . . . . 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 3122	. . . . . . . . . . . . 13 |- F/_ x { x e. A | 0 <_ B }
39		nfrab1 3122	. . . . . . . . . . . . 13 |- F/_ x { x e. A | 0 <_ C }
40	38, 39	nfin 3820	. . . . . . . . . . . 12 |- F/_ x ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } )
41	40	nfcri 2758	. . . . . . . . . . 11 |- F/ x y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } )
42	33	nfeq2 2780	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
43	41, 42	nfan 1828	. . . . . . . . . 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 2689	. . . . . . . . . . 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 2632	. . . . . . . . . . 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 747	. . . . . . . . . 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 4723	. . . . . . . . 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 4730	. . . . . . . . 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 4730	. . . . . . . . 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 2654	. . . . . . . 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 2681	. . . . . . 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 5449	. . . . . . . 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 2764	. . . . . . . . . 10 |- F/_ y ( B + C )
55		nfcsb1v 3549	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ ( B + C )
56		csbeq1a 3542	. . . . . . . . . 10 |- ( x = y -> ( B + C ) = [_ y / x ]_ ( B + C ) )
57	54, 55, 56	cbvmpt 4749	. . . . . . . . 9 |- ( x e. A |-> ( B + C ) ) = ( y e. A |-> [_ y / x ]_ ( B + C ) )
58	57	reseq1i 5392	. . . . . . . 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 1843	. . . . . . . . . 10 |- F/ y ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( B + C ) )
60	55	nfeq2 2780	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ ( B + C )
61	41, 60	nfan 1828	. . . . . . . . . 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 2632	. . . . . . . . . . 11 |- ( x = y -> ( z = ( B + C ) <-> z = [_ y / x ]_ ( B + C ) ) )
63	44, 62	anbi12d 747	. . . . . . . . . 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 4723	. . . . . . . . 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 4730	. . . . . . . . 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 4730	. . . . . . . . 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 2654	. . . . . . . 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 2681	. . . . . . 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 2654	. . . . 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 2644	. . . 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 529	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( 0 <_ B <-> ( B e. RR /\ 0 <_ B ) ) )
74		elrege0 12278	. . . . . . . . . 10 |- ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
75	73, 74	syl6bbr 278	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( 0 <_ B <-> B e. ( 0 [,) +oo ) ) )
76	75	rabbidva 3188	. . . . . . . 8 |- ( ph -> { x e. A | 0 <_ B } = { x e. A | B e. ( 0 [,) +oo ) } )
77		0xr 10086	. . . . . . . . . . 11 |- 0 e. RR*
78		pnfxr 10092	. . . . . . . . . . 11 |- +oo e. RR*
79		0ltpnf 11956	. . . . . . . . . . 11 |- 0 < +oo
80		snunioo 12298	. . . . . . . . . . 11 |- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 < +oo ) -> ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo ) )
81	77, 78, 79, 80	mp3an 1424	. . . . . . . . . 10 |- ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo )
82	81	imaeq2i 5464	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( x e. A |-> B ) " ( 0 [,) +oo ) )
83		imaundi 5545	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) )
84		eqid 2622	. . . . . . . . . 10 |- ( x e. A |-> B ) = ( x e. A |-> B )
85	84	mptpreima 5628	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( 0 [,) +oo ) ) = { x e. A | B e. ( 0 [,) +oo ) }
86	82, 83, 85	3eqtr3ri 2653	. . . . . . . 8 |- { x e. A | B e. ( 0 [,) +oo ) } = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) )
87	76, 86	syl6eq 2672	. . . . . . 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 6385	. . . . . . . 8 |- ( ph -> ( x e. A |-> B ) : A --> RR )
90		mbfimasn 23401	. . . . . . . . . 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 1413	. . . . . . . . 9 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " { 0 } ) e. dom vol )
92		mbfima 23399	. . . . . . . . 9 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) e. dom vol )
93		unmbl 23305	. . . . . . . . 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 693	. . . . . . . 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 693	. . . . . . 7 |- ( ph -> ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) ) e. dom vol )
96	87, 95	eqeltrd 2701	. . . . . 6 |- ( ph -> { x e. A | 0 <_ B } e. dom vol )
97	5	biantrurd 529	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( 0 <_ C <-> ( C e. RR /\ 0 <_ C ) ) )
98		elrege0 12278	. . . . . . . . . 10 |- ( C e. ( 0 [,) +oo ) <-> ( C e. RR /\ 0 <_ C ) )
99	97, 98	syl6bbr 278	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( 0 <_ C <-> C e. ( 0 [,) +oo ) ) )
100	99	rabbidva 3188	. . . . . . . 8 |- ( ph -> { x e. A | 0 <_ C } = { x e. A | C e. ( 0 [,) +oo ) } )
101	81	imaeq2i 5464	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( x e. A |-> C ) " ( 0 [,) +oo ) )
102		imaundi 5545	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) )
103		eqid 2622	. . . . . . . . . 10 |- ( x e. A |-> C ) = ( x e. A |-> C )
104	103	mptpreima 5628	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( 0 [,) +oo ) ) = { x e. A | C e. ( 0 [,) +oo ) }
105	101, 102, 104	3eqtr3ri 2653	. . . . . . . 8 |- { x e. A | C e. ( 0 [,) +oo ) } = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) )
106	100, 105	syl6eq 2672	. . . . . . 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 6385	. . . . . . . 8 |- ( ph -> ( x e. A |-> C ) : A --> RR )
109		mbfimasn 23401	. . . . . . . . . 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 1413	. . . . . . . . 9 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " { 0 } ) e. dom vol )
111		mbfima 23399	. . . . . . . . 9 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) e. dom vol )
112		unmbl 23305	. . . . . . . . 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 693	. . . . . . . 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 693	. . . . . . 7 |- ( ph -> ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) ) e. dom vol )
115	106, 114	eqeltrd 2701	. . . . . 6 |- ( ph -> { x e. A | 0 <_ C } e. dom vol )
116		inmbl 23310	. . . . . 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 693	. . . . 5 |- ( ph -> ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol )
118		mbfres 23411	. . . . 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 693	. . . 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 2705	. . 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 3834	. . . . . 6 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C }
122		resabs1 5427	. . . . . 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 3116	. . . . . . . . . 10 |- ( x e. { x e. A | -. 0 <_ B } <-> ( x e. A /\ -. 0 <_ B ) )
125	124, 19	anbi12i 733	. . . . . . . . 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 3796	. . . . . . . . 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 871	. . . . . . . . 9 |- ( ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) <-> ( ( x e. A /\ -. 0 <_ B ) /\ ( x e. A /\ 0 <_ C ) ) )
128	125, 126, 127	3bitr4i 292	. . . . . . . 8 |- ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) <-> ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) )
129		iffalse 4095	. . . . . . . . . . 11 |- ( -. 0 <_ B -> if ( 0 <_ B , B , 0 ) = 0 )
130	129, 23	oveqan12d 6669	. . . . . . . . . 10 |- ( ( -. 0 <_ B /\ 0 <_ C ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( 0 + C ) )
131	130	ad2antll 765	. . . . . . . . 9 |- ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( 0 + C ) )
132	5	recnd 10068	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> C e. CC )
133	132	addid2d 10237	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( 0 + C ) = C )
134	133	adantrr 753	. . . . . . . . 9 |- ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( 0 + C ) = C )
135	131, 134	eqtrd 2656	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = C )
136	128, 135	sylan2b 492	. . . . . . 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 4744	. . . . . 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 3833	. . . . . . . 8 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | -. 0 <_ B }
139		ssrab2 3687	. . . . . . . 8 |- { x e. A | -. 0 <_ B } C_ A
140	138, 139	sstri 3612	. . . . . . 7 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A
141		resmpt 5449	. . . . . . . 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 5392	. . . . . . . 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 1843	. . . . . . . . . 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 3122	. . . . . . . . . . . . 13 |- F/_ x { x e. A | -. 0 <_ B }
145	144, 39	nfin 3820	. . . . . . . . . . . 12 |- F/_ x ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } )
146	145	nfcri 2758	. . . . . . . . . . 11 |- F/ x y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } )
147	146, 42	nfan 1828	. . . . . . . . . 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 2689	. . . . . . . . . . 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 747	. . . . . . . . . 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 4723	. . . . . . . . 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 4730	. . . . . . . . 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 4730	. . . . . . . . 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 2654	. . . . . . . 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 2681	. . . . . . 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 5449	. . . . . . . 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 2764	. . . . . . . . . 10 |- F/_ y C
158		nfcsb1v 3549	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ C
159		csbeq1a 3542	. . . . . . . . . 10 |- ( x = y -> C = [_ y / x ]_ C )
160	157, 158, 159	cbvmpt 4749	. . . . . . . . 9 |- ( x e. A |-> C ) = ( y e. A |-> [_ y / x ]_ C )
161	160	reseq1i 5392	. . . . . . . 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 1843	. . . . . . . . . 10 |- F/ y ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = C )
163	158	nfeq2 2780	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ C
164	146, 163	nfan 1828	. . . . . . . . . 10 |- F/ x ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ C )
165	159	eqeq2d 2632	. . . . . . . . . . 11 |- ( x = y -> ( z = C <-> z = [_ y / x ]_ C ) )
166	148, 165	anbi12d 747	. . . . . . . . . 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 4723	. . . . . . . . 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 4730	. . . . . . . . 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 4730	. . . . . . . . 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 2654	. . . . . . . 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 2681	. . . . . . 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 2681	. . . . 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 2668	. . . 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 5628	. . . . . . . 8 |- ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) = { x e. A | B e. ( -oo (,) 0 ) }
176		elioomnf 12268	. . . . . . . . . . 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 529	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( B < 0 <-> ( B e. RR /\ B < 0 ) ) )
179		ltnle 10117	. . . . . . . . . . . 12 |- ( ( B e. RR /\ 0 e. RR ) -> ( B < 0 <-> -. 0 <_ B ) )
180	1, 2, 179	sylancl 694	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( B < 0 <-> -. 0 <_ B ) )
181	178, 180	bitr3d 270	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( ( B e. RR /\ B < 0 ) <-> -. 0 <_ B ) )
182	177, 181	syl5bb 272	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( B e. ( -oo (,) 0 ) <-> -. 0 <_ B ) )
183	182	rabbidva 3188	. . . . . . . 8 |- ( ph -> { x e. A | B e. ( -oo (,) 0 ) } = { x e. A | -. 0 <_ B } )
184	175, 183	syl5eq 2668	. . . . . . 7 |- ( ph -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) = { x e. A | -. 0 <_ B } )
185		mbfima 23399	. . . . . . . 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 693	. . . . . . 7 |- ( ph -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) e. dom vol )
187	184, 186	eqeltrrd 2702	. . . . . 6 |- ( ph -> { x e. A | -. 0 <_ B } e. dom vol )
188		inmbl 23310	. . . . . 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 693	. . . . 5 |- ( ph -> ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol )
190		mbfres 23411	. . . . 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 693	. . . 4 |- ( ph -> ( ( x e. A |-> C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) e. MblFn )
192	174, 191	eqeltrd 2701	. . 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 3624	. . . . . 6 |- A C_ A
194		dfrab3ss 3905	. . . . . 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 3961	. . . . . 6 |- A = ( { x e. A | 0 <_ B } u. { x e. A | -. 0 <_ B } )
197	196	ineq1i 3810	. . . . 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 3875	. . . . 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 2649	. . . 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 23412	. 2 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) e. MblFn )
202		rabid 3116	. . . . . 6 |- ( x e. { x e. A | -. 0 <_ C } <-> ( x e. A /\ -. 0 <_ C ) )
203		iffalse 4095	. . . . . . . . 9 |- ( -. 0 <_ C -> if ( 0 <_ C , C , 0 ) = 0 )
204	203	oveq2d 6666	. . . . . . . 8 |- ( -. 0 <_ C -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( if ( 0 <_ B , B , 0 ) + 0 ) )
205	4	recnd 10068	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. CC )
206	205	addid1d 10236	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + 0 ) = if ( 0 <_ B , B , 0 ) )
207	204, 206	sylan9eqr 2678	. . . . . . 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 679	. . . . . 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 492	. . . . 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 4744	. . . 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 3687	. . . . 5 |- { x e. A | -. 0 <_ C } C_ A
212		resmpt 5449	. . . . . 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 5392	. . . . . 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 1843	. . . . . . . 8 |- F/ y ( x e. { x e. A | -. 0 <_ C } /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
215		nfrab1 3122	. . . . . . . . . 10 |- F/_ x { x e. A | -. 0 <_ C }
216	215	nfcri 2758	. . . . . . . . 9 |- F/ x y e. { x e. A | -. 0 <_ C }
217	216, 42	nfan 1828	. . . . . . . 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 2689	. . . . . . . . 9 |- ( x = y -> ( x e. { x e. A | -. 0 <_ C } <-> y e. { x e. A | -. 0 <_ C } ) )
219	218, 45	anbi12d 747	. . . . . . . 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 4723	. . . . . . 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 4730	. . . . . . 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 4730	. . . . . . 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 2654	. . . . . 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 2681	. . . . 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 5449	. . . . . 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 2764	. . . . . . . 8 |- F/_ y if ( 0 <_ B , B , 0 )
228		nfcsb1v 3549	. . . . . . . 8 |- F/_ x [_ y / x ]_ if ( 0 <_ B , B , 0 )
229		csbeq1a 3542	. . . . . . . 8 |- ( x = y -> if ( 0 <_ B , B , 0 ) = [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
230	227, 228, 229	cbvmpt 4749	. . . . . . 7 |- ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( y e. A |-> [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
231	230	reseq1i 5392	. . . . . 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 1843	. . . . . . . 8 |- F/ y ( x e. { x e. A | -. 0 <_ C } /\ z = if ( 0 <_ B , B , 0 ) )
233	228	nfeq2 2780	. . . . . . . . 9 |- F/ x z = [_ y / x ]_ if ( 0 <_ B , B , 0 )
234	216, 233	nfan 1828	. . . . . . . 8 |- F/ x ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
235	229	eqeq2d 2632	. . . . . . . . 9 |- ( x = y -> ( z = if ( 0 <_ B , B , 0 ) <-> z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) ) )
236	218, 235	anbi12d 747	. . . . . . . 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 4723	. . . . . . 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 4730	. . . . . . 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 4730	. . . . . . 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 2654	. . . . . 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 2681	. . . . 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 2681	. . 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 23418	. . . 4 |- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
245	103	mptpreima 5628	. . . . . 6 |- ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) = { x e. A | C e. ( -oo (,) 0 ) }
246		elioomnf 12268	. . . . . . . . 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 529	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( C < 0 <-> ( C e. RR /\ C < 0 ) ) )
249		ltnle 10117	. . . . . . . . . 10 |- ( ( C e. RR /\ 0 e. RR ) -> ( C < 0 <-> -. 0 <_ C ) )
250	5, 2, 249	sylancl 694	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( C < 0 <-> -. 0 <_ C ) )
251	248, 250	bitr3d 270	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( ( C e. RR /\ C < 0 ) <-> -. 0 <_ C ) )
252	247, 251	syl5bb 272	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( C e. ( -oo (,) 0 ) <-> -. 0 <_ C ) )
253	252	rabbidva 3188	. . . . . 6 |- ( ph -> { x e. A | C e. ( -oo (,) 0 ) } = { x e. A | -. 0 <_ C } )
254	245, 253	syl5eq 2668	. . . . 5 |- ( ph -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) = { x e. A | -. 0 <_ C } )
255		mbfima 23399	. . . . . 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 693	. . . . 5 |- ( ph -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) e. dom vol )
257	254, 256	eqeltrrd 2702	. . . 4 |- ( ph -> { x e. A | -. 0 <_ C } e. dom vol )
258		mbfres 23411	. . . 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 693	. . 3 |- ( ph -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) |` { x e. A | -. 0 <_ C } ) e. MblFn )
260	243, 259	eqeltrd 2701	. 2 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | -. 0 <_ C } ) e. MblFn )
261		rabxm 3961	. . . 4 |- A = ( { x e. A | 0 <_ C } u. { x e. A | -. 0 <_ C } )
262	261	eqcomi 2631	. . 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 23412	1 |- ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) e. MblFn )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   {crab 2916   [_csb 3533   u. cun 3572   i^i cin 3573   C_ wss 3574   ifcif 4086   {csn 4177   class class class wbr 4653   {copab 4712   |-> cmpt 4729   `'ccnv 5113   dom cdm 5114   |` cres 5116   "cima 5117   -->wf 5884  (class class class)co 6650   RRcr 9935   0cc0 9936   + caddc 9939   +oocpnf 10071   -oocmnf 10072   RR*cxr 10073   < clt 10074   <_ cle 10075   (,)cioo 12175   [,)cico 12177   volcvol 23232  MblFncmbf 23383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-q 11789  df-rp 11833  df-xadd 11947  df-ioo 12179  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417  df-xmet 19739  df-met 19740  df-ovol 23233  df-vol 23234  df-mbf 23388

This theorem is referenced by:  itgaddnclem2  33469