Theorem mbfposadd 29637

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 9592	. . . . 5 |- 0 e. RR
3		ifcl 3981	. . . . 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 3981	. . . . 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 9619	. . 3 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR )
9		eqid 2467	. . 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 6043	. 2 |- ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) : A --> RR )
11		ssrab2 3585	. . . 4 |- { x e. A | 0 <_ C } C_ A
12		fssres 5749	. . . 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 3719	. . . . . 6 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C }
15		resabs1 5300	. . . . . 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 3687	. . . . . . . . 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 3038	. . . . . . . . . 10 |- ( x e. { x e. A | 0 <_ B } <-> ( x e. A /\ 0 <_ B ) )
19		rabid 3038	. . . . . . . . . 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 3945	. . . . . . . . . 10 |- ( 0 <_ B -> if ( 0 <_ B , B , 0 ) = B )
23		iftrue 3945	. . . . . . . . . 10 |- ( 0 <_ C -> if ( 0 <_ C , C , 0 ) = C )
24	22, 23	oveqan12d 6301	. . . . . . . . 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 4529	. . . . . 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 3718	. . . . . . . 8 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ B }
29		ssrab2 3585	. . . . . . . 8 |- { x e. A | 0 <_ B } C_ A
30	28, 29	sstri 3513	. . . . . . 7 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A
31		resmpt 5321	. . . . . . . 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 2629	. . . . . . . . . 10 |- F/_ y ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
33		nfcsb1v 3451	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
34		csbeq1a 3444	. . . . . . . . . 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 4537	. . . . . . . . 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 5267	. . . . . . . 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 1683	. . . . . . . . . 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 3042	. . . . . . . . . . . . 13 |- F/_ x { x e. A | 0 <_ B }
39		nfrab1 3042	. . . . . . . . . . . . 13 |- F/_ x { x e. A | 0 <_ C }
40	38, 39	nfin 3705	. . . . . . . . . . . 12 |- F/_ x ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } )
41	40	nfel2 2647	. . . . . . . . . . 11 |- F/ x y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } )
42	33	nfeq2 2646	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
43	41, 42	nfan 1875	. . . . . . . . . 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		id 22	. . . . . . . . . . . 12 |- ( x = y -> x = y )
45		eqidd 2468	. . . . . . . . . . . 12 |- ( x = y -> ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) = ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) )
46	44, 45	eleq12d 2549	. . . . . . . . . . 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 } ) ) )
47	34	eqeq2d 2481	. . . . . . . . . . 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 ) ) ) )
48	46, 47	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 ) ) ) ) )
49	37, 43, 48	cbvopab1 4517	. . . . . . . . 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 ) ) ) }
50		df-mpt 4507	. . . . . . . . 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 ) ) ) }
51		df-mpt 4507	. . . . . . . . 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 ) ) ) }
52	49, 50, 51	3eqtr4i 2506	. . . . . . . 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 ) ) )
53	31, 36, 52	3eqtr4g 2533	. . . . . . 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 ) ) ) )
54	30, 53	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 ) ) )
55		resmpt 5321	. . . . . . . 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 ) ) )
56		nfcv 2629	. . . . . . . . . 10 |- F/_ y ( B + C )
57		nfcsb1v 3451	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ ( B + C )
58		csbeq1a 3444	. . . . . . . . . 10 |- ( x = y -> ( B + C ) = [_ y / x ]_ ( B + C ) )
59	56, 57, 58	cbvmpt 4537	. . . . . . . . 9 |- ( x e. A |-> ( B + C ) ) = ( y e. A |-> [_ y / x ]_ ( B + C ) )
60	59	reseq1i 5267	. . . . . . . 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 } ) )
61		nfv 1683	. . . . . . . . . 10 |- F/ y ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( B + C ) )
62	57	nfeq2 2646	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ ( B + C )
63	41, 62	nfan 1875	. . . . . . . . . 10 |- F/ x ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( B + C ) )
64		eqidd 2468	. . . . . . . . . . . 12 |- ( x = y -> z = z )
65	64, 58	eqeq12d 2489	. . . . . . . . . . 11 |- ( x = y -> ( z = ( B + C ) <-> z = [_ y / x ]_ ( B + C ) ) )
66	46, 65	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 ) ) ) )
67	61, 63, 66	cbvopab1 4517	. . . . . . . . 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 ) ) }
68		df-mpt 4507	. . . . . . . . 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 ) ) }
69		df-mpt 4507	. . . . . . . . 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 ) ) }
70	67, 68, 69	3eqtr4i 2506	. . . . . . . 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 ) )
71	55, 60, 70	3eqtr4g 2533	. . . . . . 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 ) ) )
72	30, 71	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 ) )
73	27, 54, 72	3eqtr4i 2506	. . . . 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 } ) )
74	16, 73	eqtri 2496	. . . 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 } ) )
75		mbfposadd.5	. . . . 5 |- ( ph -> ( x e. A |-> ( B + C ) ) e. MblFn )
76	1	biantrurd 508	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( 0 <_ B <-> ( B e. RR /\ 0 <_ B ) ) )
77		elrege0 11623	. . . . . . . . . 10 |- ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
78	76, 77	syl6bbr 263	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( 0 <_ B <-> B e. ( 0 [,) +oo ) ) )
79	78	rabbidva 3104	. . . . . . . 8 |- ( ph -> { x e. A | 0 <_ B } = { x e. A | B e. ( 0 [,) +oo ) } )
80		0xr 9636	. . . . . . . . . . 11 |- 0 e. RR*
81		pnfxr 11317	. . . . . . . . . . 11 |- +oo e. RR*
82		0ltpnf 11328	. . . . . . . . . . 11 |- 0 < +oo
83		snunioo 11642	. . . . . . . . . . 11 |- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 < +oo ) -> ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo ) )
84	80, 81, 82, 83	mp3an 1324	. . . . . . . . . 10 |- ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo )
85	84	imaeq2i 5333	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( x e. A |-> B ) " ( 0 [,) +oo ) )
86		imaundi 5416	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) )
87		eqid 2467	. . . . . . . . . 10 |- ( x e. A |-> B ) = ( x e. A |-> B )
88	87	mptpreima 5498	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( 0 [,) +oo ) ) = { x e. A | B e. ( 0 [,) +oo ) }
89	85, 86, 88	3eqtr3ri 2505	. . . . . . . 8 |- { x e. A | B e. ( 0 [,) +oo ) } = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) )
90	79, 89	syl6eq 2524	. . . . . . 7 |- ( ph -> { x e. A | 0 <_ B } = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) ) )
91		mbfposadd.1	. . . . . . . 8 |- ( ph -> ( x e. A |-> B ) e. MblFn )
92	1, 87	fmptd 6043	. . . . . . . 8 |- ( ph -> ( x e. A |-> B ) : A --> RR )
93		mbfimasn 21773	. . . . . . . . . 10 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR /\ 0 e. RR ) -> ( `' ( x e. A |-> B ) " { 0 } ) e. dom vol )
94	2, 93	mp3an3 1313	. . . . . . . . 9 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " { 0 } ) e. dom vol )
95		mbfima 21771	. . . . . . . . 9 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) e. dom vol )
96		unmbl 21680	. . . . . . . . 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 )
97	94, 95, 96	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 )
98	91, 92, 97	syl2anc 661	. . . . . . 7 |- ( ph -> ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) ) e. dom vol )
99	90, 98	eqeltrd 2555	. . . . . 6 |- ( ph -> { x e. A | 0 <_ B } e. dom vol )
100	5	biantrurd 508	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( 0 <_ C <-> ( C e. RR /\ 0 <_ C ) ) )
101		elrege0 11623	. . . . . . . . . 10 |- ( C e. ( 0 [,) +oo ) <-> ( C e. RR /\ 0 <_ C ) )
102	100, 101	syl6bbr 263	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( 0 <_ C <-> C e. ( 0 [,) +oo ) ) )
103	102	rabbidva 3104	. . . . . . . 8 |- ( ph -> { x e. A | 0 <_ C } = { x e. A | C e. ( 0 [,) +oo ) } )
104	84	imaeq2i 5333	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( x e. A |-> C ) " ( 0 [,) +oo ) )
105		imaundi 5416	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) )
106		eqid 2467	. . . . . . . . . 10 |- ( x e. A |-> C ) = ( x e. A |-> C )
107	106	mptpreima 5498	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( 0 [,) +oo ) ) = { x e. A | C e. ( 0 [,) +oo ) }
108	104, 105, 107	3eqtr3ri 2505	. . . . . . . 8 |- { x e. A | C e. ( 0 [,) +oo ) } = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) )
109	103, 108	syl6eq 2524	. . . . . . 7 |- ( ph -> { x e. A | 0 <_ C } = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) ) )
110		mbfposadd.3	. . . . . . . 8 |- ( ph -> ( x e. A |-> C ) e. MblFn )
111	5, 106	fmptd 6043	. . . . . . . 8 |- ( ph -> ( x e. A |-> C ) : A --> RR )
112		mbfimasn 21773	. . . . . . . . . 10 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR /\ 0 e. RR ) -> ( `' ( x e. A |-> C ) " { 0 } ) e. dom vol )
113	2, 112	mp3an3 1313	. . . . . . . . 9 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " { 0 } ) e. dom vol )
114		mbfima 21771	. . . . . . . . 9 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) e. dom vol )
115		unmbl 21680	. . . . . . . . 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 )
116	113, 114, 115	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 )
117	110, 111, 116	syl2anc 661	. . . . . . 7 |- ( ph -> ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) ) e. dom vol )
118	109, 117	eqeltrd 2555	. . . . . 6 |- ( ph -> { x e. A | 0 <_ C } e. dom vol )
119		inmbl 21684	. . . . . 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 )
120	99, 118, 119	syl2anc 661	. . . . 5 |- ( ph -> ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol )
121		mbfres 21783	. . . . 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 )
122	75, 120, 121	syl2anc 661	. . . 4 |- ( ph -> ( ( x e. A |-> ( B + C ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) e. MblFn )
123	74, 122	syl5eqel 2559	. . 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 )
124		inss2 3719	. . . . . 6 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C }
125		resabs1 5300	. . . . . 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 } ) ) )
126	124, 125	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 } ) )
127		rabid 3038	. . . . . . . . . 10 |- ( x e. { x e. A | -. 0 <_ B } <-> ( x e. A /\ -. 0 <_ B ) )
128	127, 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 ) ) )
129		elin 3687	. . . . . . . . 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 } ) )
130		anandi 826	. . . . . . . . 9 |- ( ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) <-> ( ( x e. A /\ -. 0 <_ B ) /\ ( x e. A /\ 0 <_ C ) ) )
131	128, 129, 130	3bitr4i 277	. . . . . . . 8 |- ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) <-> ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) )
132		iffalse 3948	. . . . . . . . . . 11 |- ( -. 0 <_ B -> if ( 0 <_ B , B , 0 ) = 0 )
133	132, 23	oveqan12d 6301	. . . . . . . . . 10 |- ( ( -. 0 <_ B /\ 0 <_ C ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( 0 + C ) )
134	133	ad2antll 728	. . . . . . . . 9 |- ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( 0 + C ) )
135	5	recnd 9618	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> C e. CC )
136	135	addid2d 9776	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( 0 + C ) = C )
137	136	adantrr 716	. . . . . . . . 9 |- ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( 0 + C ) = C )
138	134, 137	eqtrd 2508	. . . . . . . 8 |- ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = C )
139	131, 138	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 )
140	139	mpteq2dva 4533	. . . . . 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 ) )
141		inss1 3718	. . . . . . . 8 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | -. 0 <_ B }
142		ssrab2 3585	. . . . . . . 8 |- { x e. A | -. 0 <_ B } C_ A
143	141, 142	sstri 3513	. . . . . . 7 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A
144		resmpt 5321	. . . . . . . 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 ) ) ) )
145	35	reseq1i 5267	. . . . . . . 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 } ) )
146		nfv 1683	. . . . . . . . . 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 ) ) )
147		nfrab1 3042	. . . . . . . . . . . . 13 |- F/_ x { x e. A | -. 0 <_ B }
148	147, 39	nfin 3705	. . . . . . . . . . . 12 |- F/_ x ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } )
149	148	nfel2 2647	. . . . . . . . . . 11 |- F/ x y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } )
150	149, 42	nfan 1875	. . . . . . . . . 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 ) ) )
151		eqidd 2468	. . . . . . . . . . . 12 |- ( x = y -> ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) = ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) )
152	44, 151	eleq12d 2549	. . . . . . . . . . 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 } ) ) )
153	152, 47	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 ) ) ) ) )
154	146, 150, 153	cbvopab1 4517	. . . . . . . . 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 ) ) ) }
155		df-mpt 4507	. . . . . . . . 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 ) ) ) }
156		df-mpt 4507	. . . . . . . . 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 ) ) ) }
157	154, 155, 156	3eqtr4i 2506	. . . . . . . 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 ) ) )
158	144, 145, 157	3eqtr4g 2533	. . . . . . 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 ) ) ) )
159	143, 158	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 ) ) )
160		resmpt 5321	. . . . . . . 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 ) )
161		nfcv 2629	. . . . . . . . . 10 |- F/_ y C
162		nfcsb1v 3451	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ C
163		csbeq1a 3444	. . . . . . . . . 10 |- ( x = y -> C = [_ y / x ]_ C )
164	161, 162, 163	cbvmpt 4537	. . . . . . . . 9 |- ( x e. A |-> C ) = ( y e. A |-> [_ y / x ]_ C )
165	164	reseq1i 5267	. . . . . . . 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 } ) )
166		nfv 1683	. . . . . . . . . 10 |- F/ y ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = C )
167	162	nfeq2 2646	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ C
168	149, 167	nfan 1875	. . . . . . . . . 10 |- F/ x ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ C )
169	64, 163	eqeq12d 2489	. . . . . . . . . . 11 |- ( x = y -> ( z = C <-> z = [_ y / x ]_ C ) )
170	152, 169	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 ) ) )
171	166, 168, 170	cbvopab1 4517	. . . . . . . . 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 ) }
172		df-mpt 4507	. . . . . . . . 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 ) }
173		df-mpt 4507	. . . . . . . . 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 ) }
174	171, 172, 173	3eqtr4i 2506	. . . . . . . 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 )
175	160, 165, 174	3eqtr4g 2533	. . . . . . 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 ) )
176	143, 175	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 )
177	140, 159, 176	3eqtr4g 2533	. . . . 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 } ) ) )
178	126, 177	syl5eq 2520	. . . 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 } ) ) )
179	87	mptpreima 5498	. . . . . . . 8 |- ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) = { x e. A | B e. ( -oo (,) 0 ) }
180		elioomnf 11615	. . . . . . . . . . 11 |- ( 0 e. RR* -> ( B e. ( -oo (,) 0 ) <-> ( B e. RR /\ B < 0 ) ) )
181	80, 180	ax-mp 5	. . . . . . . . . 10 |- ( B e. ( -oo (,) 0 ) <-> ( B e. RR /\ B < 0 ) )
182	1	biantrurd 508	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( B < 0 <-> ( B e. RR /\ B < 0 ) ) )
183		ltnle 9660	. . . . . . . . . . . 12 |- ( ( B e. RR /\ 0 e. RR ) -> ( B < 0 <-> -. 0 <_ B ) )
184	1, 2, 183	sylancl 662	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( B < 0 <-> -. 0 <_ B ) )
185	182, 184	bitr3d 255	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( ( B e. RR /\ B < 0 ) <-> -. 0 <_ B ) )
186	181, 185	syl5bb 257	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( B e. ( -oo (,) 0 ) <-> -. 0 <_ B ) )
187	186	rabbidva 3104	. . . . . . . 8 |- ( ph -> { x e. A | B e. ( -oo (,) 0 ) } = { x e. A | -. 0 <_ B } )
188	179, 187	syl5eq 2520	. . . . . . 7 |- ( ph -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) = { x e. A | -. 0 <_ B } )
189		mbfima 21771	. . . . . . . 8 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) e. dom vol )
190	91, 92, 189	syl2anc 661	. . . . . . 7 |- ( ph -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) e. dom vol )
191	188, 190	eqeltrrd 2556	. . . . . 6 |- ( ph -> { x e. A | -. 0 <_ B } e. dom vol )
192		inmbl 21684	. . . . . 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 )
193	191, 118, 192	syl2anc 661	. . . . 5 |- ( ph -> ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol )
194		mbfres 21783	. . . . 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 )
195	110, 193, 194	syl2anc 661	. . . 4 |- ( ph -> ( ( x e. A |-> C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) e. MblFn )
196	178, 195	eqeltrd 2555	. . 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 )
197		ssid 3523	. . . . . 6 |- A C_ A
198		dfrab3ss 3776	. . . . . 6 |- ( A C_ A -> { x e. A | 0 <_ C } = ( A i^i { x e. A | 0 <_ C } ) )
199	197, 198	ax-mp 5	. . . . 5 |- { x e. A | 0 <_ C } = ( A i^i { x e. A | 0 <_ C } )
200		rabxm 3808	. . . . . 6 |- A = ( { x e. A | 0 <_ B } u. { x e. A | -. 0 <_ B } )
201	200	ineq1i 3696	. . . . 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 } )
202		indir 3746	. . . . 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 } ) )
203	199, 201, 202	3eqtrri 2501	. . . 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 }
204	203	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 } )
205	13, 123, 196, 204	mbfres2 21784	. 2 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) e. MblFn )
206		rabid 3038	. . . . . 6 |- ( x e. { x e. A | -. 0 <_ C } <-> ( x e. A /\ -. 0 <_ C ) )
207		iffalse 3948	. . . . . . . . 9 |- ( -. 0 <_ C -> if ( 0 <_ C , C , 0 ) = 0 )
208	207	oveq2d 6298	. . . . . . . 8 |- ( -. 0 <_ C -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( if ( 0 <_ B , B , 0 ) + 0 ) )
209	4	recnd 9618	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. CC )
210	209	addid1d 9775	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + 0 ) = if ( 0 <_ B , B , 0 ) )
211	208, 210	sylan9eqr 2530	. . . . . . 7 |- ( ( ( ph /\ x e. A ) /\ -. 0 <_ C ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ B , B , 0 ) )
212	211	anasss 647	. . . . . 6 |- ( ( ph /\ ( x e. A /\ -. 0 <_ C ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ B , B , 0 ) )
213	206, 212	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 ) )
214	213	mpteq2dva 4533	. . . 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 ) ) )
215		ssrab2 3585	. . . . 5 |- { x e. A | -. 0 <_ C } C_ A
216		resmpt 5321	. . . . . 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 ) ) ) )
217	35	reseq1i 5267	. . . . . 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 } )
218		nfv 1683	. . . . . . . 8 |- F/ y ( x e. { x e. A | -. 0 <_ C } /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
219		nfrab1 3042	. . . . . . . . . 10 |- F/_ x { x e. A | -. 0 <_ C }
220	219	nfel2 2647	. . . . . . . . 9 |- F/ x y e. { x e. A | -. 0 <_ C }
221	220, 42	nfan 1875	. . . . . . . 8 |- F/ x ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
222		eleq1 2539	. . . . . . . . 9 |- ( x = y -> ( x e. { x e. A | -. 0 <_ C } <-> y e. { x e. A | -. 0 <_ C } ) )
223	222, 47	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 ) ) ) ) )
224	218, 221, 223	cbvopab1 4517	. . . . . . 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 ) ) ) }
225		df-mpt 4507	. . . . . . 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 ) ) ) }
226		df-mpt 4507	. . . . . . 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 ) ) ) }
227	224, 225, 226	3eqtr4i 2506	. . . . . 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 ) ) )
228	216, 217, 227	3eqtr4g 2533	. . . . 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 ) ) ) )
229	215, 228	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 ) ) )
230		resmpt 5321	. . . . . 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 ) ) )
231		nfcv 2629	. . . . . . . 8 |- F/_ y if ( 0 <_ B , B , 0 )
232		nfcsb1v 3451	. . . . . . . 8 |- F/_ x [_ y / x ]_ if ( 0 <_ B , B , 0 )
233		csbeq1a 3444	. . . . . . . 8 |- ( x = y -> if ( 0 <_ B , B , 0 ) = [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
234	231, 232, 233	cbvmpt 4537	. . . . . . 7 |- ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( y e. A |-> [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
235	234	reseq1i 5267	. . . . . 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 } )
236		nfv 1683	. . . . . . . 8 |- F/ y ( x e. { x e. A | -. 0 <_ C } /\ z = if ( 0 <_ B , B , 0 ) )
237	232	nfeq2 2646	. . . . . . . . 9 |- F/ x z = [_ y / x ]_ if ( 0 <_ B , B , 0 )
238	220, 237	nfan 1875	. . . . . . . 8 |- F/ x ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
239	233	eqeq2d 2481	. . . . . . . . 9 |- ( x = y -> ( z = if ( 0 <_ B , B , 0 ) <-> z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) ) )
240	222, 239	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 ) ) ) )
241	236, 238, 240	cbvopab1 4517	. . . . . . 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 ) ) }
242		df-mpt 4507	. . . . . . 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 ) ) }
243		df-mpt 4507	. . . . . . 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 ) ) }
244	241, 242, 243	3eqtr4i 2506	. . . . . 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 ) )
245	230, 235, 244	3eqtr4g 2533	. . . . 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 ) ) )
246	215, 245	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 ) )
247	214, 229, 246	3eqtr4g 2533	. . 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 } ) )
248	1, 91	mbfpos 21790	. . . 4 |- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
249	106	mptpreima 5498	. . . . . 6 |- ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) = { x e. A | C e. ( -oo (,) 0 ) }
250		elioomnf 11615	. . . . . . . . 9 |- ( 0 e. RR* -> ( C e. ( -oo (,) 0 ) <-> ( C e. RR /\ C < 0 ) ) )
251	80, 250	ax-mp 5	. . . . . . . 8 |- ( C e. ( -oo (,) 0 ) <-> ( C e. RR /\ C < 0 ) )
252	5	biantrurd 508	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( C < 0 <-> ( C e. RR /\ C < 0 ) ) )
253		ltnle 9660	. . . . . . . . . 10 |- ( ( C e. RR /\ 0 e. RR ) -> ( C < 0 <-> -. 0 <_ C ) )
254	5, 2, 253	sylancl 662	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( C < 0 <-> -. 0 <_ C ) )
255	252, 254	bitr3d 255	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( ( C e. RR /\ C < 0 ) <-> -. 0 <_ C ) )
256	251, 255	syl5bb 257	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( C e. ( -oo (,) 0 ) <-> -. 0 <_ C ) )
257	256	rabbidva 3104	. . . . . 6 |- ( ph -> { x e. A | C e. ( -oo (,) 0 ) } = { x e. A | -. 0 <_ C } )
258	249, 257	syl5eq 2520	. . . . 5 |- ( ph -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) = { x e. A | -. 0 <_ C } )
259		mbfima 21771	. . . . . 6 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) e. dom vol )
260	110, 111, 259	syl2anc 661	. . . . 5 |- ( ph -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) e. dom vol )
261	258, 260	eqeltrrd 2556	. . . 4 |- ( ph -> { x e. A | -. 0 <_ C } e. dom vol )
262		mbfres 21783	. . . 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 )
263	248, 261, 262	syl2anc 661	. . 3 |- ( ph -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) |` { x e. A | -. 0 <_ C } ) e. MblFn )
264	247, 263	eqeltrd 2555	. 2 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | -. 0 <_ C } ) e. MblFn )
265		rabxm 3808	. . . 4 |- A = ( { x e. A | 0 <_ C } u. { x e. A | -. 0 <_ C } )
266	265	eqcomi 2480	. . 3 |- ( { x e. A | 0 <_ C } u. { x e. A | -. 0 <_ C } ) = A
267	266	a1i 11	. 2 |- ( ph -> ( { x e. A | 0 <_ C } u. { x e. A | -. 0 <_ C } ) = A )
268	10, 205, 264, 267	mbfres2 21784	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 1379   e. wcel 1767   {crab 2818   [_csb 3435   u. cun 3474   i^i cin 3475   C_ wss 3476   ifcif 3939   {csn 4027   class class class wbr 4447   {copab 4504   |-> cmpt 4505   `'ccnv 4998   dom cdm 4999   |` cres 5001   "cima 5002   -->wf 5582  (class class class)co 6282   RRcr 9487   0cc0 9488   + caddc 9491   +oocpnf 9621   -oocmnf 9622   RR*cxr 9623   < clt 9624   <_ cle 9625   (,)cioo 11525   [,)cico 11527   volcvol 21607  MblFncmbf 21755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-inf2 8054  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565  ax-pre-sup 9566

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-isom 5595  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-of 6522  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-2o 7128  df-oadd 7131  df-er 7308  df-map 7419  df-pm 7420  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-sup 7897  df-oi 7931  df-card 8316  df-cda 8544  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-div 10203  df-nn 10533  df-2 10590  df-3 10591  df-n0 10792  df-z 10861  df-uz 11079  df-q 11179  df-rp 11217  df-xadd 11315  df-ioo 11529  df-ico 11531  df-icc 11532  df-fz 11669  df-fzo 11789  df-fl 11893  df-seq 12071  df-exp 12130  df-hash 12368  df-cj 12889  df-re 12890  df-im 12891  df-sqrt 13025  df-abs 13026  df-clim 13267  df-sum 13465  df-xmet 18180  df-met 18181  df-ovol 21608  df-vol 21609  df-mbf 21760

This theorem is referenced by:  itgaddnclem2  29649