Metamath Proof Explorer

Theorem mbfposadd

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)

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

Proof

Step Hyp Ref Expression
1 mbfposadd.1 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
2 mbfposadd.2 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
3 mbfposadd.3 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
4 mbfposadd.4 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
5 mbfposadd.5 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. MblFn )
6 0re 
 |-  0 e. RR
7 ifcl 
 |-  ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
8 2 6 7 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
9 ifcl 
 |-  ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
10 4 6 9 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
11 8 10 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR )
12 11 fmpttd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) : A --> RR )
13 ssrab2 
 |-  { x e. A | 0 <_ C } C_ A
14 fssres 
 |-  ( ( ( 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 )
15 12 13 14 sylancl 
 |-  ( 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 )
16 inss2 
 |-  ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C }
17 resabs1 
 |-  ( ( { 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 } ) ) )
18 16 17 ax-mp 
 |-  ( ( ( 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 } ) )
19 elin 
 |-  ( 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 } ) )
20 rabid 
 |-  ( x e. { x e. A | 0 <_ B } <-> ( x e. A /\ 0 <_ B ) )
21 rabid 
 |-  ( x e. { x e. A | 0 <_ C } <-> ( x e. A /\ 0 <_ C ) )
22 20 21 anbi12i 
 |-  ( ( x e. { x e. A | 0 <_ B } /\ x e. { x e. A | 0 <_ C } ) <-> ( ( x e. A /\ 0 <_ B ) /\ ( x e. A /\ 0 <_ C ) ) )
23 19 22 bitri 
 |-  ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) <-> ( ( x e. A /\ 0 <_ B ) /\ ( x e. A /\ 0 <_ C ) ) )
24 iftrue 
 |-  ( 0 <_ B -> if ( 0 <_ B , B , 0 ) = B )
25 iftrue 
 |-  ( 0 <_ C -> if ( 0 <_ C , C , 0 ) = C )
26 24 25 oveqan12d 
 |-  ( ( 0 <_ B /\ 0 <_ C ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( B + C ) )
27 26 ad2ant2l 
 |-  ( ( ( x e. A /\ 0 <_ B ) /\ ( x e. A /\ 0 <_ C ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( B + C ) )
28 23 27 sylbi 
 |-  ( 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 ) )
29 28 mpteq2ia 
 |-  ( 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 ) )
30 inss1 
 |-  ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ B }
31 ssrab2 
 |-  { x e. A | 0 <_ B } C_ A
32 30 31 sstri 
 |-  ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A
33 resmpt 
 |-  ( ( { 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 ) ) ) )
34 nfcv 
 |-  F/_ y ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
35 nfcsb1v 
 |-  F/_ x [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
36 csbeq1a 
 |-  ( x = y -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
37 34 35 36 cbvmpt 
 |-  ( 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 ) ) )
38 37 reseq1i 
 |-  ( ( 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 } ) )
39 nfv 
 |-  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 ) ) )
40 nfrab1 
 |-  F/_ x { x e. A | 0 <_ B }
41 nfrab1 
 |-  F/_ x { x e. A | 0 <_ C }
42 40 41 nfin 
 |-  F/_ x ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } )
43 42 nfcri 
 |-  F/ x y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } )
44 35 nfeq2 
 |-  F/ x z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) )
45 43 44 nfan 
 |-  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 ) ) )
46 eleq1w 
 |-  ( 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 36 eqeq2d 
 |-  ( 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 
 |-  ( 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 39 45 48 cbvopab1 
 |-  { <. 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 33 38 52 3eqtr4g 
 |-  ( ( { 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 32 53 ax-mp 
 |-  ( ( 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 
 |-  ( ( { 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 
 |-  F/_ y ( B + C )
57 nfcsb1v 
 |-  F/_ x [_ y / x ]_ ( B + C )
58 csbeq1a 
 |-  ( x = y -> ( B + C ) = [_ y / x ]_ ( B + C ) )
59 56 57 58 cbvmpt 
 |-  ( x e. A |-> ( B + C ) ) = ( y e. A |-> [_ y / x ]_ ( B + C ) )
60 59 reseq1i 
 |-  ( ( 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 
 |-  F/ y ( x e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = ( B + C ) )
62 57 nfeq2 
 |-  F/ x z = [_ y / x ]_ ( B + C )
63 43 62 nfan 
 |-  F/ x ( y e. ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ ( B + C ) )
64 58 eqeq2d 
 |-  ( x = y -> ( z = ( B + C ) <-> z = [_ y / x ]_ ( B + C ) ) )
65 46 64 anbi12d 
 |-  ( 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 ) ) ) )
66 61 63 65 cbvopab1 
 |-  { <. 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 ) ) }
67 df-mpt 
 |-  ( 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 ) ) }
68 df-mpt 
 |-  ( 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 ) ) }
69 66 67 68 3eqtr4i 
 |-  ( 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 ) )
70 55 60 69 3eqtr4g 
 |-  ( ( { 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 ) ) )
71 32 70 ax-mp 
 |-  ( ( 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 29 54 71 3eqtr4i 
 |-  ( ( 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 } ) )
73 18 72 eqtri 
 |-  ( ( ( 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 } ) )
74 2 biantrurd 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ B <-> ( B e. RR /\ 0 <_ B ) ) )
75 elrege0 
 |-  ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
76 74 75 bitr4di 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ B <-> B e. ( 0 [,) +oo ) ) )
77 76 rabbidva 
 |-  ( ph -> { x e. A | 0 <_ B } = { x e. A | B e. ( 0 [,) +oo ) } )
78 0xr 
 |-  0 e. RR*
79 pnfxr 
 |-  +oo e. RR*
80 0ltpnf 
 |-  0 < +oo
81 snunioo 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ 0 < +oo ) -> ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo ) )
82 78 79 80 81 mp3an 
 |-  ( { 0 } u. ( 0 (,) +oo ) ) = ( 0 [,) +oo )
83 82 imaeq2i 
 |-  ( `' ( x e. A |-> B ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( x e. A |-> B ) " ( 0 [,) +oo ) )
84 imaundi 
 |-  ( `' ( x e. A |-> B ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) )
85 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
86 85 mptpreima 
 |-  ( `' ( x e. A |-> B ) " ( 0 [,) +oo ) ) = { x e. A | B e. ( 0 [,) +oo ) }
87 83 84 86 3eqtr3ri 
 |-  { x e. A | B e. ( 0 [,) +oo ) } = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) )
88 77 87 eqtrdi 
 |-  ( ph -> { x e. A | 0 <_ B } = ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) ) )
89 2 fmpttd 
 |-  ( ph -> ( x e. A |-> B ) : A --> RR )
90 mbfimasn 
 |-  ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR /\ 0 e. RR ) -> ( `' ( x e. A |-> B ) " { 0 } ) e. dom vol )
91 6 90 mp3an3 
 |-  ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " { 0 } ) e. dom vol )
92 mbfima 
 |-  ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) e. dom vol )
93 unmbl 
 |-  ( ( ( `' ( 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 
 |-  ( ( ( 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 1 89 94 syl2anc 
 |-  ( ph -> ( ( `' ( x e. A |-> B ) " { 0 } ) u. ( `' ( x e. A |-> B ) " ( 0 (,) +oo ) ) ) e. dom vol )
96 88 95 eqeltrd 
 |-  ( ph -> { x e. A | 0 <_ B } e. dom vol )
97 4 biantrurd 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ C <-> ( C e. RR /\ 0 <_ C ) ) )
98 elrege0 
 |-  ( C e. ( 0 [,) +oo ) <-> ( C e. RR /\ 0 <_ C ) )
99 97 98 bitr4di 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ C <-> C e. ( 0 [,) +oo ) ) )
100 99 rabbidva 
 |-  ( ph -> { x e. A | 0 <_ C } = { x e. A | C e. ( 0 [,) +oo ) } )
101 82 imaeq2i 
 |-  ( `' ( x e. A |-> C ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( `' ( x e. A |-> C ) " ( 0 [,) +oo ) )
102 imaundi 
 |-  ( `' ( x e. A |-> C ) " ( { 0 } u. ( 0 (,) +oo ) ) ) = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) )
103 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
104 103 mptpreima 
 |-  ( `' ( x e. A |-> C ) " ( 0 [,) +oo ) ) = { x e. A | C e. ( 0 [,) +oo ) }
105 101 102 104 3eqtr3ri 
 |-  { x e. A | C e. ( 0 [,) +oo ) } = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) )
106 100 105 eqtrdi 
 |-  ( ph -> { x e. A | 0 <_ C } = ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) ) )
107 4 fmpttd 
 |-  ( ph -> ( x e. A |-> C ) : A --> RR )
108 mbfimasn 
 |-  ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR /\ 0 e. RR ) -> ( `' ( x e. A |-> C ) " { 0 } ) e. dom vol )
109 6 108 mp3an3 
 |-  ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " { 0 } ) e. dom vol )
110 mbfima 
 |-  ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) e. dom vol )
111 unmbl 
 |-  ( ( ( `' ( 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 )
112 109 110 111 syl2anc 
 |-  ( ( ( 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 )
113 3 107 112 syl2anc 
 |-  ( ph -> ( ( `' ( x e. A |-> C ) " { 0 } ) u. ( `' ( x e. A |-> C ) " ( 0 (,) +oo ) ) ) e. dom vol )
114 106 113 eqeltrd 
 |-  ( ph -> { x e. A | 0 <_ C } e. dom vol )
115 inmbl 
 |-  ( ( { 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 )
116 96 114 115 syl2anc 
 |-  ( ph -> ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol )
117 mbfres 
 |-  ( ( ( 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 )
118 5 116 117 syl2anc 
 |-  ( ph -> ( ( x e. A |-> ( B + C ) ) |` ( { x e. A | 0 <_ B } i^i { x e. A | 0 <_ C } ) ) e. MblFn )
119 73 118 eqeltrid 
 |-  ( 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 )
120 inss2 
 |-  ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | 0 <_ C }
121 resabs1 
 |-  ( ( { 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 } ) ) )
122 120 121 ax-mp 
 |-  ( ( ( 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 rabid 
 |-  ( x e. { x e. A | -. 0 <_ B } <-> ( x e. A /\ -. 0 <_ B ) )
124 123 21 anbi12i 
 |-  ( ( x e. { x e. A | -. 0 <_ B } /\ x e. { x e. A | 0 <_ C } ) <-> ( ( x e. A /\ -. 0 <_ B ) /\ ( x e. A /\ 0 <_ C ) ) )
125 elin 
 |-  ( 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 } ) )
126 anandi 
 |-  ( ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) <-> ( ( x e. A /\ -. 0 <_ B ) /\ ( x e. A /\ 0 <_ C ) ) )
127 124 125 126 3bitr4i 
 |-  ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) <-> ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) )
128 iffalse 
 |-  ( -. 0 <_ B -> if ( 0 <_ B , B , 0 ) = 0 )
129 128 25 oveqan12d 
 |-  ( ( -. 0 <_ B /\ 0 <_ C ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( 0 + C ) )
130 129 ad2antll 
 |-  ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( 0 + C ) )
131 4 recnd 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
132 131 addlidd 
 |-  ( ( ph /\ x e. A ) -> ( 0 + C ) = C )
133 132 adantrr 
 |-  ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( 0 + C ) = C )
134 130 133 eqtrd 
 |-  ( ( ph /\ ( x e. A /\ ( -. 0 <_ B /\ 0 <_ C ) ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = C )
135 127 134 sylan2b 
 |-  ( ( 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 )
136 135 mpteq2dva 
 |-  ( 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 ) )
137 inss1 
 |-  ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ { x e. A | -. 0 <_ B }
138 ssrab2 
 |-  { x e. A | -. 0 <_ B } C_ A
139 137 138 sstri 
 |-  ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) C_ A
140 resmpt 
 |-  ( ( { 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 ) ) ) )
141 37 reseq1i 
 |-  ( ( 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 } ) )
142 nfv 
 |-  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 ) ) )
143 nfrab1 
 |-  F/_ x { x e. A | -. 0 <_ B }
144 143 41 nfin 
 |-  F/_ x ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } )
145 144 nfcri 
 |-  F/ x y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } )
146 145 44 nfan 
 |-  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 ) ) )
147 eleq1w 
 |-  ( 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 } ) ) )
148 147 47 anbi12d 
 |-  ( 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 ) ) ) ) )
149 142 146 148 cbvopab1 
 |-  { <. 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 ) ) ) }
150 df-mpt 
 |-  ( 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 ) ) ) }
151 df-mpt 
 |-  ( 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 ) ) ) }
152 149 150 151 3eqtr4i 
 |-  ( 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 ) ) )
153 140 141 152 3eqtr4g 
 |-  ( ( { 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 ) ) ) )
154 139 153 ax-mp 
 |-  ( ( 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 resmpt 
 |-  ( ( { 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 ) )
156 nfcv 
 |-  F/_ y C
157 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
158 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
159 156 157 158 cbvmpt 
 |-  ( x e. A |-> C ) = ( y e. A |-> [_ y / x ]_ C )
160 159 reseq1i 
 |-  ( ( 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 } ) )
161 nfv 
 |-  F/ y ( x e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = C )
162 157 nfeq2 
 |-  F/ x z = [_ y / x ]_ C
163 145 162 nfan 
 |-  F/ x ( y e. ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) /\ z = [_ y / x ]_ C )
164 158 eqeq2d 
 |-  ( x = y -> ( z = C <-> z = [_ y / x ]_ C ) )
165 147 164 anbi12d 
 |-  ( 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 ) ) )
166 161 163 165 cbvopab1 
 |-  { <. 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 ) }
167 df-mpt 
 |-  ( 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 ) }
168 df-mpt 
 |-  ( 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 ) }
169 166 167 168 3eqtr4i 
 |-  ( 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 )
170 155 160 169 3eqtr4g 
 |-  ( ( { 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 ) )
171 139 170 ax-mp 
 |-  ( ( 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 136 154 171 3eqtr4g 
 |-  ( 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 } ) ) )
173 122 172 eqtrid 
 |-  ( 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 } ) ) )
174 85 mptpreima 
 |-  ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) = { x e. A | B e. ( -oo (,) 0 ) }
175 elioomnf 
 |-  ( 0 e. RR* -> ( B e. ( -oo (,) 0 ) <-> ( B e. RR /\ B < 0 ) ) )
176 78 175 ax-mp 
 |-  ( B e. ( -oo (,) 0 ) <-> ( B e. RR /\ B < 0 ) )
177 2 biantrurd 
 |-  ( ( ph /\ x e. A ) -> ( B < 0 <-> ( B e. RR /\ B < 0 ) ) )
178 ltnle 
 |-  ( ( B e. RR /\ 0 e. RR ) -> ( B < 0 <-> -. 0 <_ B ) )
179 2 6 178 sylancl 
 |-  ( ( ph /\ x e. A ) -> ( B < 0 <-> -. 0 <_ B ) )
180 177 179 bitr3d 
 |-  ( ( ph /\ x e. A ) -> ( ( B e. RR /\ B < 0 ) <-> -. 0 <_ B ) )
181 176 180 bitrid 
 |-  ( ( ph /\ x e. A ) -> ( B e. ( -oo (,) 0 ) <-> -. 0 <_ B ) )
182 181 rabbidva 
 |-  ( ph -> { x e. A | B e. ( -oo (,) 0 ) } = { x e. A | -. 0 <_ B } )
183 174 182 eqtrid 
 |-  ( ph -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) = { x e. A | -. 0 <_ B } )
184 mbfima 
 |-  ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) e. dom vol )
185 1 89 184 syl2anc 
 |-  ( ph -> ( `' ( x e. A |-> B ) " ( -oo (,) 0 ) ) e. dom vol )
186 183 185 eqeltrrd 
 |-  ( ph -> { x e. A | -. 0 <_ B } e. dom vol )
187 inmbl 
 |-  ( ( { 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 )
188 186 114 187 syl2anc 
 |-  ( ph -> ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) e. dom vol )
189 mbfres 
 |-  ( ( ( 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 )
190 3 188 189 syl2anc 
 |-  ( ph -> ( ( x e. A |-> C ) |` ( { x e. A | -. 0 <_ B } i^i { x e. A | 0 <_ C } ) ) e. MblFn )
191 173 190 eqeltrd 
 |-  ( 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 )
192 ssid 
 |-  A C_ A
193 dfrab3ss 
 |-  ( A C_ A -> { x e. A | 0 <_ C } = ( A i^i { x e. A | 0 <_ C } ) )
194 192 193 ax-mp 
 |-  { x e. A | 0 <_ C } = ( A i^i { x e. A | 0 <_ C } )
195 rabxm 
 |-  A = ( { x e. A | 0 <_ B } u. { x e. A | -. 0 <_ B } )
196 195 ineq1i 
 |-  ( 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 } )
197 indir 
 |-  ( ( { 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 } ) )
198 194 196 197 3eqtrri 
 |-  ( ( { 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 }
199 198 a1i 
 |-  ( 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 } )
200 15 119 191 199 mbfres2 
 |-  ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | 0 <_ C } ) e. MblFn )
201 rabid 
 |-  ( x e. { x e. A | -. 0 <_ C } <-> ( x e. A /\ -. 0 <_ C ) )
202 iffalse 
 |-  ( -. 0 <_ C -> if ( 0 <_ C , C , 0 ) = 0 )
203 202 oveq2d 
 |-  ( -. 0 <_ C -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = ( if ( 0 <_ B , B , 0 ) + 0 ) )
204 8 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. CC )
205 204 addridd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + 0 ) = if ( 0 <_ B , B , 0 ) )
206 203 205 sylan9eqr 
 |-  ( ( ( ph /\ x e. A ) /\ -. 0 <_ C ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ B , B , 0 ) )
207 206 anasss 
 |-  ( ( ph /\ ( x e. A /\ -. 0 <_ C ) ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ B , B , 0 ) )
208 201 207 sylan2b 
 |-  ( ( ph /\ x e. { x e. A | -. 0 <_ C } ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) = if ( 0 <_ B , B , 0 ) )
209 208 mpteq2dva 
 |-  ( 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 ) ) )
210 ssrab2 
 |-  { x e. A | -. 0 <_ C } C_ A
211 resmpt 
 |-  ( { 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 ) ) ) )
212 37 reseq1i 
 |-  ( ( 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 } )
213 nfv 
 |-  F/ y ( x e. { x e. A | -. 0 <_ C } /\ z = ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
214 nfrab1 
 |-  F/_ x { x e. A | -. 0 <_ C }
215 214 nfcri 
 |-  F/ x y e. { x e. A | -. 0 <_ C }
216 215 44 nfan 
 |-  F/ x ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
217 eleq1w 
 |-  ( x = y -> ( x e. { x e. A | -. 0 <_ C } <-> y e. { x e. A | -. 0 <_ C } ) )
218 217 47 anbi12d 
 |-  ( 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 ) ) ) ) )
219 213 216 218 cbvopab1 
 |-  { <. 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 ) ) ) }
220 df-mpt 
 |-  ( 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 ) ) ) }
221 df-mpt 
 |-  ( 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 ) ) ) }
222 219 220 221 3eqtr4i 
 |-  ( 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 ) ) )
223 211 212 222 3eqtr4g 
 |-  ( { 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 ) ) ) )
224 210 223 ax-mp 
 |-  ( ( 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 resmpt 
 |-  ( { 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 ) ) )
226 nfcv 
 |-  F/_ y if ( 0 <_ B , B , 0 )
227 nfcsb1v 
 |-  F/_ x [_ y / x ]_ if ( 0 <_ B , B , 0 )
228 csbeq1a 
 |-  ( x = y -> if ( 0 <_ B , B , 0 ) = [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
229 226 227 228 cbvmpt 
 |-  ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( y e. A |-> [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
230 229 reseq1i 
 |-  ( ( 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 } )
231 nfv 
 |-  F/ y ( x e. { x e. A | -. 0 <_ C } /\ z = if ( 0 <_ B , B , 0 ) )
232 227 nfeq2 
 |-  F/ x z = [_ y / x ]_ if ( 0 <_ B , B , 0 )
233 215 232 nfan 
 |-  F/ x ( y e. { x e. A | -. 0 <_ C } /\ z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) )
234 228 eqeq2d 
 |-  ( x = y -> ( z = if ( 0 <_ B , B , 0 ) <-> z = [_ y / x ]_ if ( 0 <_ B , B , 0 ) ) )
235 217 234 anbi12d 
 |-  ( 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 ) ) ) )
236 231 233 235 cbvopab1 
 |-  { <. 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 ) ) }
237 df-mpt 
 |-  ( 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 ) ) }
238 df-mpt 
 |-  ( 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 ) ) }
239 236 237 238 3eqtr4i 
 |-  ( 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 ) )
240 225 230 239 3eqtr4g 
 |-  ( { 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 ) ) )
241 210 240 ax-mp 
 |-  ( ( 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 209 224 241 3eqtr4g 
 |-  ( 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 } ) )
243 2 1 mbfpos 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
244 103 mptpreima 
 |-  ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) = { x e. A | C e. ( -oo (,) 0 ) }
245 elioomnf 
 |-  ( 0 e. RR* -> ( C e. ( -oo (,) 0 ) <-> ( C e. RR /\ C < 0 ) ) )
246 78 245 ax-mp 
 |-  ( C e. ( -oo (,) 0 ) <-> ( C e. RR /\ C < 0 ) )
247 4 biantrurd 
 |-  ( ( ph /\ x e. A ) -> ( C < 0 <-> ( C e. RR /\ C < 0 ) ) )
248 ltnle 
 |-  ( ( C e. RR /\ 0 e. RR ) -> ( C < 0 <-> -. 0 <_ C ) )
249 4 6 248 sylancl 
 |-  ( ( ph /\ x e. A ) -> ( C < 0 <-> -. 0 <_ C ) )
250 247 249 bitr3d 
 |-  ( ( ph /\ x e. A ) -> ( ( C e. RR /\ C < 0 ) <-> -. 0 <_ C ) )
251 246 250 bitrid 
 |-  ( ( ph /\ x e. A ) -> ( C e. ( -oo (,) 0 ) <-> -. 0 <_ C ) )
252 251 rabbidva 
 |-  ( ph -> { x e. A | C e. ( -oo (,) 0 ) } = { x e. A | -. 0 <_ C } )
253 244 252 eqtrid 
 |-  ( ph -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) = { x e. A | -. 0 <_ C } )
254 mbfima 
 |-  ( ( ( x e. A |-> C ) e. MblFn /\ ( x e. A |-> C ) : A --> RR ) -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) e. dom vol )
255 3 107 254 syl2anc 
 |-  ( ph -> ( `' ( x e. A |-> C ) " ( -oo (,) 0 ) ) e. dom vol )
256 253 255 eqeltrrd 
 |-  ( ph -> { x e. A | -. 0 <_ C } e. dom vol )
257 mbfres 
 |-  ( ( ( 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 )
258 243 256 257 syl2anc 
 |-  ( ph -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) |` { x e. A | -. 0 <_ C } ) e. MblFn )
259 242 258 eqeltrd 
 |-  ( ph -> ( ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) |` { x e. A | -. 0 <_ C } ) e. MblFn )
260 rabxm 
 |-  A = ( { x e. A | 0 <_ C } u. { x e. A | -. 0 <_ C } )
261 260 eqcomi 
 |-  ( { x e. A | 0 <_ C } u. { x e. A | -. 0 <_ C } ) = A
262 261 a1i 
 |-  ( ph -> ( { x e. A | 0 <_ C } u. { x e. A | -. 0 <_ C } ) = A )
263 12 200 259 262 mbfres2 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) e. MblFn )