Theorem mbfposadd 28451

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 9398	. . . . 5 |- 0 e. RR
3		ifcl 3843	. . . . 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 3843	. . . . 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 9425	. . 3 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR )
9		eqid 2443	. . 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 5879	. 2 |- ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) : A --> RR )
11		ssrab2 3449	. . . 4 |- { x e. A | 0 <_ C } C_ A
12		fssres 5590	. . . 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 3583	. . . . . 6 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C }
15		resabs1 5151	. . . . . 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 3551	. . . . . . . . 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 2909	. . . . . . . . . 10 |- ( x e. { x e. A | 0 <_ B } <-> ( x e. A /\ 0 <_ B ) )
19		rabid 2909	. . . . . . . . . 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 3809	. . . . . . . . . 10 |- ( 0 <_ B -> if ( 0 <_ B , B , 0 ) = B )
23		iftrue 3809	. . . . . . . . . 10 |- ( 0 <_ C -> if ( 0 <_ C , C , 0 ) = C )
24	22, 23	oveqan12d 6122	. . . . . . . . 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 4386	. . . . . 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 3582	. . . . . . . 8 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ B }
29		ssrab2 3449	. . . . . . . 8 |- { x e. A | 0 <_ B } C_ A
30	28, 29	sstri 3377	. . . . . . 7 |- ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A
31		resmpt 5168	. . . . . . . 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 2589	. . . . . . . . . 10 |- F/_ y ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
33		nfcsb1v 3316	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
34		csbeq1a 3309	. . . . . . . . . 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 4394	. . . . . . . . 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 5118	. . . . . . . 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 1673	. . . . . . . . . 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 2913	. . . . . . . . . . . . 13 |- F/_ x { x e. A | 0 <_ B }
39		nfrab1 2913	. . . . . . . . . . . . 13 |- F/_ x { x e. A | 0 <_ C }
40	38, 39	nfin 3569	. . . . . . . . . . . 12 |- F/_ x ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } )
41	40	nfel2 2606	. . . . . . . . . . 11 |- F/ x y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } )
42	33	nfeq2 2605	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
43	41, 42	nfan 1861	. . . . . . . . . 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 2444	. . . . . . . . . . . 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 2511	. . . . . . . . . . 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 2454	. . . . . . . . . . 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 4374	. . . . . . . . 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 4364	. . . . . . . . 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 4364	. . . . . . . . 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 2473	. . . . . . . 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 2500	. . . . . . 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 5168	. . . . . . . 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 2589	. . . . . . . . . 10 |- F/_ y ( B + C )
57		nfcsb1v 3316	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ ( B + C )
58		csbeq1a 3309	. . . . . . . . . 10 |- ( x = y -> ( B + C ) = [_ y / x ]_ ( B + C ) )
59	56, 57, 58	cbvmpt 4394	. . . . . . . . 9 |- ( x e. A |-> ( B + C ) ) = ( y e. A |-> [_ y / x ]_ ( B + C ) )
60	59	reseq1i 5118	. . . . . . . 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 1673	. . . . . . . . . 10 |- F/ y ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( B + C ) )
62	57	nfeq2 2605	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ ( B + C )
63	41, 62	nfan 1861	. . . . . . . . . 10 |- F/ x ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( B + C ) )
64		eqidd 2444	. . . . . . . . . . . 12 |- ( x = y -> z = z )
65	64, 58	eqeq12d 2457	. . . . . . . . . . 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 4374	. . . . . . . . 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 4364	. . . . . . . . 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 4364	. . . . . . . . 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 2473	. . . . . . . 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 2500	. . . . . . 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 2473	. . . . 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 2463	. . . 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 11404	. . . . . . . . . 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 2975	. . . . . . . 8 |- ( ph -> { x e. A | 0 <_ B } = { x e. A | B e. ( 0 [,) +oo ) } )
80		0xr 9442	. . . . . . . . . . 11 |- 0 e. RR*
81		pnfxr 11104	. . . . . . . . . . 11 |- +oo e. RR*
82		0ltpnf 11115	. . . . . . . . . . 11 |- 0 < +oo
83		snunioo 11423	. . . . . . . . . . 11 |- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 < +oo ) -> ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo ) )
84	80, 81, 82, 83	mp3an 1314	. . . . . . . . . 10 |- ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo )
85	84	imaeq2i 5179	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( x e. A |-> B ) " ( 0 [,) +oo ) )
86		imaundi 5261	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) )
87		eqid 2443	. . . . . . . . . 10 |- ( x e. A |-> B ) = ( x e. A |-> B )
88	87	mptpreima 5343	. . . . . . . . 9 |- ( `' ( x e. A |-> B ) " ( 0 [,) +oo ) ) = { x e. A | B e. ( 0 [,) +oo ) }
89	85, 86, 88	3eqtr3ri 2472	. . . . . . . 8 |- { x e. A | B e. ( 0 [,) +oo ) } = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) )
90	79, 89	syl6eq 2491	. . . . . . 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 5879	. . . . . . . 8 |- ( ph -> ( x e. A |-> B ) : A --> RR )
93		mbfimasn 21124	. . . . . . . . . 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 1303	. . . . . . . . 9 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " { 0 } ) e. dom vol )
95		mbfima 21122	. . . . . . . . 9 |- ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) e. dom vol )
96		unmbl 21031	. . . . . . . . 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 2517	. . . . . 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 11404	. . . . . . . . . 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 2975	. . . . . . . 8 |- ( ph -> { x e. A | 0 <_ C } = { x e. A | C e. ( 0 [,) +oo ) } )
104	84	imaeq2i 5179	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( x e. A |-> C ) " ( 0 [,) +oo ) )
105		imaundi 5261	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) )
106		eqid 2443	. . . . . . . . . 10 |- ( x e. A |-> C ) = ( x e. A |-> C )
107	106	mptpreima 5343	. . . . . . . . 9 |- ( `' ( x e. A |-> C ) " ( 0 [,) +oo ) ) = { x e. A | C e. ( 0 [,) +oo ) }
108	104, 105, 107	3eqtr3ri 2472	. . . . . . . 8 |- { x e. A | C e. ( 0 [,) +oo ) } = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) )
109	103, 108	syl6eq 2491	. . . . . . 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 5879	. . . . . . . 8 |- ( ph -> ( x e. A |-> C ) : A --> RR )
112		mbfimasn 21124	. . . . . . . . . 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 1303	. . . . . . . . 9 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " { 0 } ) e. dom vol )
114		mbfima 21122	. . . . . . . . 9 |- ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) e. dom vol )
115		unmbl 21031	. . . . . . . . 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 2517	. . . . . 6 |- ( ph -> { x e. A | 0 <_ C } e. dom vol )
119		inmbl 21035	. . . . . 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 21134	. . . . 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 2527	. . 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 3583	. . . . . 6 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C }
125		resabs1 5151	. . . . . 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 2909	. . . . . . . . . 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 3551	. . . . . . . . 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 824	. . . . . . . . 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 3811	. . . . . . . . . . 11 |- ( -. 0 <_ B -> if ( 0 <_ B , B , 0 ) = 0 )
133	132, 23	oveqan12d 6122	. . . . . . . . . 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 9424	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> C e. CC )
136	135	addid2d 9582	. . . . . . . . . 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 2475	. . . . . . . 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 4390	. . . . . 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 3582	. . . . . . . 8 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | -. 0 <_ B }
142		ssrab2 3449	. . . . . . . 8 |- { x e. A | -. 0 <_ B } C_ A
143	141, 142	sstri 3377	. . . . . . 7 |- ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A
144		resmpt 5168	. . . . . . . 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 5118	. . . . . . . 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 1673	. . . . . . . . . 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 2913	. . . . . . . . . . . . 13 |- F/_ x { x e. A | -. 0 <_ B }
148	147, 39	nfin 3569	. . . . . . . . . . . 12 |- F/_ x ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } )
149	148	nfel2 2606	. . . . . . . . . . 11 |- F/ x y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } )
150	149, 42	nfan 1861	. . . . . . . . . 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 2444	. . . . . . . . . . . 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 2511	. . . . . . . . . . 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 4374	. . . . . . . . 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 4364	. . . . . . . . 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 4364	. . . . . . . . 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 2473	. . . . . . . 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 2500	. . . . . . 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 5168	. . . . . . . 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 2589	. . . . . . . . . 10 |- F/_ y C
162		nfcsb1v 3316	. . . . . . . . . 10 |- F/_ x [_ y / x ]_ C
163		csbeq1a 3309	. . . . . . . . . 10 |- ( x = y -> C = [_ y / x ]_ C )
164	161, 162, 163	cbvmpt 4394	. . . . . . . . 9 |- ( x e. A |-> C ) = ( y e. A |-> [_ y / x ]_ C )
165	164	reseq1i 5118	. . . . . . . 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 1673	. . . . . . . . . 10 |- F/ y ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = C )
167	162	nfeq2 2605	. . . . . . . . . . 11 |- F/ x z = [_ y / x ]_ C
168	149, 167	nfan 1861	. . . . . . . . . 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 2457	. . . . . . . . . . 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 4374	. . . . . . . . 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 4364	. . . . . . . . 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 4364	. . . . . . . . 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 2473	. . . . . . . 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 2500	. . . . . . 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 2500	. . . . 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 2487	. . . 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 5343	. . . . . . . 8 |- ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) = { x e. A | B e. ( -oo (,) 0 ) }
180		elioomnf 11396	. . . . . . . . . . 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 9466	. . . . . . . . . . . 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 2975	. . . . . . . 8 |- ( ph -> { x e. A | B e. ( -oo (,) 0 ) } = { x e. A | -. 0 <_ B } )
188	179, 187	syl5eq 2487	. . . . . . 7 |- ( ph -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) = { x e. A | -. 0 <_ B } )
189		mbfima 21122	. . . . . . . 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 2518	. . . . . 6 |- ( ph -> { x e. A | -. 0 <_ B } e. dom vol )
192		inmbl 21035	. . . . . 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 21134	. . . . 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 2517	. . 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 3387	. . . . . 6 |- A C_ A
198		dfrab3ss 3640	. . . . . 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 3672	. . . . . 6 |- A = ( { x e. A | 0 <_ B } u. { x e. A | -. 0 <_ B } )
201	200	ineq1i 3560	. . . . 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 3610	. . . . 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 2468	. . . 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 21135	. 2 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) e. MblFn )
206		rabid 2909	. . . . . 6 |- ( x e. { x e. A | -. 0 <_ C } <-> ( x e. A /\ -. 0 <_ C ) )
207		iffalse 3811	. . . . . . . . 9 |- ( -. 0 <_ C -> if ( 0 <_ C , C , 0 ) = 0 )
208	207	oveq2d 6119	. . . . . . . 8 |- ( -. 0 <_ C -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( if ( 0 <_ B , B , 0 ) + 0 ) )
209	4	recnd 9424	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. CC )
210	209	addid1d 9581	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + 0 ) = if ( 0 <_ B , B , 0 ) )
211	208, 210	sylan9eqr 2497	. . . . . . 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 4390	. . . 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 3449	. . . . 5 |- { x e. A | -. 0 <_ C } C_ A
216		resmpt 5168	. . . . . 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 5118	. . . . . 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 1673	. . . . . . . 8 |- F/ y ( x e. { x e. A | -. 0 <_ C } /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
219		nfrab1 2913	. . . . . . . . . 10 |- F/_ x { x e. A | -. 0 <_ C }
220	219	nfel2 2606	. . . . . . . . 9 |- F/ x y e. { x e. A | -. 0 <_ C }
221	220, 42	nfan 1861	. . . . . . . 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 2503	. . . . . . . . 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 4374	. . . . . . 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 4364	. . . . . . 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 4364	. . . . . . 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 2473	. . . . . 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 2500	. . . . 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 5168	. . . . . 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 2589	. . . . . . . 8 |- F/_ y if ( 0 <_ B , B , 0 )
232		nfcsb1v 3316	. . . . . . . 8 |- F/_ x [_ y / x ]_ if ( 0 <_ B , B , 0 )
233		csbeq1a 3309	. . . . . . . 8 |- ( x = y -> if ( 0 <_ B , B , 0 ) = [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
234	231, 232, 233	cbvmpt 4394	. . . . . . 7 |- ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( y e. A |-> [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
235	234	reseq1i 5118	. . . . . 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 1673	. . . . . . . 8 |- F/ y ( x e. { x e. A | -. 0 <_ C } /\ z = if ( 0 <_ B , B , 0 ) )
237	232	nfeq2 2605	. . . . . . . . 9 |- F/ x z = [_ y / x ]_ if ( 0 <_ B , B , 0 )
238	220, 237	nfan 1861	. . . . . . . 8 |- F/ x ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
239	233	eqeq2d 2454	. . . . . . . . 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 4374	. . . . . . 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 4364	. . . . . . 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 4364	. . . . . . 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 2473	. . . . . 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 2500	. . . . 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 2500	. . 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 21141	. . . 4 |- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
249	106	mptpreima 5343	. . . . . 6 |- ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) = { x e. A | C e. ( -oo (,) 0 ) }
250		elioomnf 11396	. . . . . . . . 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 9466	. . . . . . . . . 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 2975	. . . . . 6 |- ( ph -> { x e. A | C e. ( -oo (,) 0 ) } = { x e. A | -. 0 <_ C } )
258	249, 257	syl5eq 2487	. . . . 5 |- ( ph -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) = { x e. A | -. 0 <_ C } )
259		mbfima 21122	. . . . . 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 2518	. . . 4 |- ( ph -> { x e. A | -. 0 <_ C } e. dom vol )
262		mbfres 21134	. . . 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 2517	. 2 |- ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | -. 0 <_ C } ) e. MblFn )
265		rabxm 3672	. . . 4 |- A = ( { x e. A | 0 <_ C } u. { x e. A | -. 0 <_ C } )
266	265	eqcomi 2447	. . 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 21135	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 1369   e. wcel 1756   {crab 2731   [_csb 3300   u. cun 3338   i^i cin 3339   C_ wss 3340   ifcif 3803   {csn 3889   class class class wbr 4304   {copab 4361   e. cmpt 4362   `'ccnv 4851   dom cdm 4852   |` cres 4854   "cima 4855   -->wf 5426  (class class class)co 6103   RRcr 9293   0cc0 9294   + caddc 9297   +oocpnf 9427   -oocmnf 9428   RR*cxr 9429   < clt 9430   <_ cle 9431   (,)cioo 11312   [,)cico 11314   volcvol 20959  MblFncmbf 21106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4415  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384  ax-inf2 7859  ax-cnex 9350  ax-resscn 9351  ax-1cn 9352  ax-icn 9353  ax-addcl 9354  ax-addrcl 9355  ax-mulcl 9356  ax-mulrcl 9357  ax-mulcom 9358  ax-addass 9359  ax-mulass 9360  ax-distr 9361  ax-i2m1 9362  ax-1ne0 9363  ax-1rid 9364  ax-rnegex 9365  ax-rrecex 9366  ax-cnre 9367  ax-pre-lttri 9368  ax-pre-lttrn 9369  ax-pre-ltadd 9370  ax-pre-mulgt0 9371  ax-pre-sup 9372

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-nel 2621  df-ral 2732  df-rex 2733  df-reu 2734  df-rmo 2735  df-rab 2736  df-v 2986  df-sbc 3199  df-csb 3301  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-pss 3356  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-tp 3894  df-op 3896  df-uni 4104  df-int 4141  df-iun 4185  df-br 4305  df-opab 4363  df-mpt 4364  df-tr 4398  df-eprel 4644  df-id 4648  df-po 4653  df-so 4654  df-fr 4691  df-se 4692  df-we 4693  df-ord 4734  df-on 4735  df-lim 4736  df-suc 4737  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-fo 5436  df-f1o 5437  df-fv 5438  df-isom 5439  df-riota 6064  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-of 6332  df-om 6489  df-1st 6589  df-2nd 6590  df-recs 6844  df-rdg 6878  df-1o 6932  df-2o 6933  df-oadd 6936  df-er 7113  df-map 7228  df-pm 7229  df-en 7323  df-dom 7324  df-sdom 7325  df-fin 7326  df-sup 7703  df-oi 7736  df-card 8121  df-cda 8349  df-pnf 9432  df-mnf 9433  df-xr 9434  df-ltxr 9435  df-le 9436  df-sub 9609  df-neg 9610  df-div 10006  df-nn 10335  df-2 10392  df-3 10393  df-n0 10592  df-z 10659  df-uz 10874  df-q 10966  df-rp 11004  df-xadd 11102  df-ioo 11316  df-ico 11318  df-icc 11319  df-fz 11450  df-fzo 11561  df-fl 11654  df-seq 11819  df-exp 11878  df-hash 12116  df-cj 12600  df-re 12601  df-im 12602  df-sqr 12736  df-abs 12737  df-clim 12978  df-sum 13176  df-xmet 17822  df-met 17823  df-ovol 20960  df-vol 20961  df-mbf 21111

This theorem is referenced by:  itgaddnclem2  28463