Metamath Proof Explorer

Theorem mbfposr

Description: Converse to mbfpos . (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses mbfpos.1 
|- ( ( ph /\ x e. A ) -> B e. RR )
mbfposr.2 
|- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
mbfposr.3 
|- ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn )
Assertion mbfposr 
|- ( ph -> ( x e. A |-> B ) e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfpos.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
2 mbfposr.2 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
3 mbfposr.3 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn )
4 1 fmpttd 
 |-  ( ph -> ( x e. A |-> B ) : A --> RR )
5 0re 
 |-  0 e. RR
6 ifcl 
 |-  ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
7 1 5 6 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
8 2 7 mbfdm2 
 |-  ( ph -> A e. dom vol )
9 simplr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> y < 0 )
10 simpllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> y e. RR )
11 10 lt0neg1d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( y < 0 <-> 0 < -u y ) )
12 9 11 mpbid 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> 0 < -u y )
13 12 biantrurd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( -u B < -u y <-> ( 0 < -u y /\ -u B < -u y ) ) )
14 1 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> B e. RR )
15 10 14 ltnegd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( y < B <-> -u B < -u y ) )
16 0red 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> 0 e. RR )
17 14 renegcld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> -u B e. RR )
18 10 renegcld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> -u y e. RR )
19 maxlt 
 |-  ( ( 0 e. RR /\ -u B e. RR /\ -u y e. RR ) -> ( if ( 0 <_ -u B , -u B , 0 ) < -u y <-> ( 0 < -u y /\ -u B < -u y ) ) )
20 16 17 18 19 syl3anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) < -u y <-> ( 0 < -u y /\ -u B < -u y ) ) )
21 13 15 20 3bitr4rd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) < -u y <-> y < B ) )
22 1 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. RR )
23 ifcl 
 |-  ( ( -u B e. RR /\ 0 e. RR ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
24 22 5 23 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
25 24 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
26 25 biantrurd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) < -u y <-> ( if ( 0 <_ -u B , -u B , 0 ) e. RR /\ if ( 0 <_ -u B , -u B , 0 ) < -u y ) ) )
27 14 biantrurd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( y < B <-> ( B e. RR /\ y < B ) ) )
28 21 26 27 3bitr3d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( ( if ( 0 <_ -u B , -u B , 0 ) e. RR /\ if ( 0 <_ -u B , -u B , 0 ) < -u y ) <-> ( B e. RR /\ y < B ) ) )
29 18 rexrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> -u y e. RR* )
30 elioomnf 
 |-  ( -u y e. RR* -> ( if ( 0 <_ -u B , -u B , 0 ) e. ( -oo (,) -u y ) <-> ( if ( 0 <_ -u B , -u B , 0 ) e. RR /\ if ( 0 <_ -u B , -u B , 0 ) < -u y ) ) )
31 29 30 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) e. ( -oo (,) -u y ) <-> ( if ( 0 <_ -u B , -u B , 0 ) e. RR /\ if ( 0 <_ -u B , -u B , 0 ) < -u y ) ) )
32 10 rexrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> y e. RR* )
33 elioopnf 
 |-  ( y e. RR* -> ( B e. ( y (,) +oo ) <-> ( B e. RR /\ y < B ) ) )
34 32 33 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( B e. ( y (,) +oo ) <-> ( B e. RR /\ y < B ) ) )
35 28 31 34 3bitr4d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) e. ( -oo (,) -u y ) <-> B e. ( y (,) +oo ) ) )
36 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
37 eqid 
 |-  ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) = ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) )
38 37 fvmpt2 
 |-  ( ( x e. A /\ if ( 0 <_ -u B , -u B , 0 ) e. RR ) -> ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) = if ( 0 <_ -u B , -u B , 0 ) )
39 36 24 38 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) = if ( 0 <_ -u B , -u B , 0 ) )
40 39 eleq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -oo (,) -u y ) <-> if ( 0 <_ -u B , -u B , 0 ) e. ( -oo (,) -u y ) ) )
41 40 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -oo (,) -u y ) <-> if ( 0 <_ -u B , -u B , 0 ) e. ( -oo (,) -u y ) ) )
42 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
43 42 fvmpt2 
 |-  ( ( x e. A /\ B e. RR ) -> ( ( x e. A |-> B ) ` x ) = B )
44 36 1 43 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = B )
45 44 eleq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) e. ( y (,) +oo ) <-> B e. ( y (,) +oo ) ) )
46 45 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) e. ( y (,) +oo ) <-> B e. ( y (,) +oo ) ) )
47 35 41 46 3bitr4d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y < 0 ) /\ x e. A ) -> ( ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -oo (,) -u y ) <-> ( ( x e. A |-> B ) ` x ) e. ( y (,) +oo ) ) )
48 47 pm5.32da 
 |-  ( ( ( ph /\ y e. RR ) /\ y < 0 ) -> ( ( x e. A /\ ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -oo (,) -u y ) ) <-> ( x e. A /\ ( ( x e. A |-> B ) ` x ) e. ( y (,) +oo ) ) ) )
49 24 fmpttd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) : A --> RR )
50 ffn 
 |-  ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) : A --> RR -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) Fn A )
51 elpreima 
 |-  ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) Fn A -> ( x e. ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -oo (,) -u y ) ) <-> ( x e. A /\ ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -oo (,) -u y ) ) ) )
52 49 50 51 3syl 
 |-  ( ph -> ( x e. ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -oo (,) -u y ) ) <-> ( x e. A /\ ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -oo (,) -u y ) ) ) )
53 52 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ y < 0 ) -> ( x e. ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -oo (,) -u y ) ) <-> ( x e. A /\ ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -oo (,) -u y ) ) ) )
54 ffn 
 |-  ( ( x e. A |-> B ) : A --> RR -> ( x e. A |-> B ) Fn A )
55 elpreima 
 |-  ( ( x e. A |-> B ) Fn A -> ( x e. ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) <-> ( x e. A /\ ( ( x e. A |-> B ) ` x ) e. ( y (,) +oo ) ) ) )
56 4 54 55 3syl 
 |-  ( ph -> ( x e. ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) <-> ( x e. A /\ ( ( x e. A |-> B ) ` x ) e. ( y (,) +oo ) ) ) )
57 56 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ y < 0 ) -> ( x e. ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) <-> ( x e. A /\ ( ( x e. A |-> B ) ` x ) e. ( y (,) +oo ) ) ) )
58 48 53 57 3bitr4d 
 |-  ( ( ( ph /\ y e. RR ) /\ y < 0 ) -> ( x e. ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -oo (,) -u y ) ) <-> x e. ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) ) )
59 58 alrimiv 
 |-  ( ( ( ph /\ y e. RR ) /\ y < 0 ) -> A. x ( x e. ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -oo (,) -u y ) ) <-> x e. ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) ) )
60 nfmpt1 
 |-  F/_ x ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) )
61 60 nfcnv 
 |-  F/_ x `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) )
62 nfcv 
 |-  F/_ x ( -oo (,) -u y )
63 61 62 nfima 
 |-  F/_ x ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -oo (,) -u y ) )
64 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
65 64 nfcnv 
 |-  F/_ x `' ( x e. A |-> B )
66 nfcv 
 |-  F/_ x ( y (,) +oo )
67 65 66 nfima 
 |-  F/_ x ( `' ( x e. A |-> B ) " ( y (,) +oo ) )
68 63 67 cleqf 
 |-  ( ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -oo (,) -u y ) ) = ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) <-> A. x ( x e. ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -oo (,) -u y ) ) <-> x e. ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) ) )
69 59 68 sylibr 
 |-  ( ( ( ph /\ y e. RR ) /\ y < 0 ) -> ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -oo (,) -u y ) ) = ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) )
70 mbfima 
 |-  ( ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) : A --> RR ) -> ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -oo (,) -u y ) ) e. dom vol )
71 3 49 70 syl2anc 
 |-  ( ph -> ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -oo (,) -u y ) ) e. dom vol )
72 71 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ y < 0 ) -> ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -oo (,) -u y ) ) e. dom vol )
73 69 72 eqeltrrd 
 |-  ( ( ( ph /\ y e. RR ) /\ y < 0 ) -> ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) e. dom vol )
74 simplr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> 0 <_ y )
75 0red 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> 0 e. RR )
76 1 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> B e. RR )
77 simpllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> y e. RR )
78 maxle 
 |-  ( ( 0 e. RR /\ B e. RR /\ y e. RR ) -> ( if ( 0 <_ B , B , 0 ) <_ y <-> ( 0 <_ y /\ B <_ y ) ) )
79 75 76 77 78 syl3anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) <_ y <-> ( 0 <_ y /\ B <_ y ) ) )
80 74 79 mpbirand 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) <_ y <-> B <_ y ) )
81 80 notbid 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( -. if ( 0 <_ B , B , 0 ) <_ y <-> -. B <_ y ) )
82 76 5 6 sylancl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
83 77 82 ltnled 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( y < if ( 0 <_ B , B , 0 ) <-> -. if ( 0 <_ B , B , 0 ) <_ y ) )
84 77 76 ltnled 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( y < B <-> -. B <_ y ) )
85 81 83 84 3bitr4d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( y < if ( 0 <_ B , B , 0 ) <-> y < B ) )
86 82 biantrurd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( y < if ( 0 <_ B , B , 0 ) <-> ( if ( 0 <_ B , B , 0 ) e. RR /\ y < if ( 0 <_ B , B , 0 ) ) ) )
87 76 biantrurd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( y < B <-> ( B e. RR /\ y < B ) ) )
88 85 86 87 3bitr3d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( ( if ( 0 <_ B , B , 0 ) e. RR /\ y < if ( 0 <_ B , B , 0 ) ) <-> ( B e. RR /\ y < B ) ) )
89 77 rexrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> y e. RR* )
90 elioopnf 
 |-  ( y e. RR* -> ( if ( 0 <_ B , B , 0 ) e. ( y (,) +oo ) <-> ( if ( 0 <_ B , B , 0 ) e. RR /\ y < if ( 0 <_ B , B , 0 ) ) ) )
91 89 90 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) e. ( y (,) +oo ) <-> ( if ( 0 <_ B , B , 0 ) e. RR /\ y < if ( 0 <_ B , B , 0 ) ) ) )
92 89 33 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( B e. ( y (,) +oo ) <-> ( B e. RR /\ y < B ) ) )
93 88 91 92 3bitr4d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) e. ( y (,) +oo ) <-> B e. ( y (,) +oo ) ) )
94 eqid 
 |-  ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( x e. A |-> if ( 0 <_ B , B , 0 ) )
95 94 fvmpt2 
 |-  ( ( x e. A /\ if ( 0 <_ B , B , 0 ) e. RR ) -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) = if ( 0 <_ B , B , 0 ) )
96 36 7 95 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) = if ( 0 <_ B , B , 0 ) )
97 96 eleq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( y (,) +oo ) <-> if ( 0 <_ B , B , 0 ) e. ( y (,) +oo ) ) )
98 97 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( y (,) +oo ) <-> if ( 0 <_ B , B , 0 ) e. ( y (,) +oo ) ) )
99 45 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) e. ( y (,) +oo ) <-> B e. ( y (,) +oo ) ) )
100 93 98 99 3bitr4d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) /\ x e. A ) -> ( ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( y (,) +oo ) <-> ( ( x e. A |-> B ) ` x ) e. ( y (,) +oo ) ) )
101 100 pm5.32da 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) -> ( ( x e. A /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( y (,) +oo ) ) <-> ( x e. A /\ ( ( x e. A |-> B ) ` x ) e. ( y (,) +oo ) ) ) )
102 7 fmpttd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) : A --> RR )
103 ffn 
 |-  ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) : A --> RR -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) Fn A )
104 elpreima 
 |-  ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) Fn A -> ( x e. ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( y (,) +oo ) ) <-> ( x e. A /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( y (,) +oo ) ) ) )
105 102 103 104 3syl 
 |-  ( ph -> ( x e. ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( y (,) +oo ) ) <-> ( x e. A /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( y (,) +oo ) ) ) )
106 105 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) -> ( x e. ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( y (,) +oo ) ) <-> ( x e. A /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( y (,) +oo ) ) ) )
107 56 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) -> ( x e. ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) <-> ( x e. A /\ ( ( x e. A |-> B ) ` x ) e. ( y (,) +oo ) ) ) )
108 101 106 107 3bitr4d 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) -> ( x e. ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( y (,) +oo ) ) <-> x e. ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) ) )
109 108 alrimiv 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) -> A. x ( x e. ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( y (,) +oo ) ) <-> x e. ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) ) )
110 nfmpt1 
 |-  F/_ x ( x e. A |-> if ( 0 <_ B , B , 0 ) )
111 110 nfcnv 
 |-  F/_ x `' ( x e. A |-> if ( 0 <_ B , B , 0 ) )
112 111 66 nfima 
 |-  F/_ x ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( y (,) +oo ) )
113 112 67 cleqf 
 |-  ( ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( y (,) +oo ) ) = ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) <-> A. x ( x e. ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( y (,) +oo ) ) <-> x e. ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) ) )
114 109 113 sylibr 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) -> ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( y (,) +oo ) ) = ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) )
115 mbfima 
 |-  ( ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ B , B , 0 ) ) : A --> RR ) -> ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( y (,) +oo ) ) e. dom vol )
116 2 102 115 syl2anc 
 |-  ( ph -> ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( y (,) +oo ) ) e. dom vol )
117 116 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) -> ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( y (,) +oo ) ) e. dom vol )
118 114 117 eqeltrrd 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 <_ y ) -> ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) e. dom vol )
119 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
120 0red 
 |-  ( ( ph /\ y e. RR ) -> 0 e. RR )
121 73 118 119 120 ltlecasei 
 |-  ( ( ph /\ y e. RR ) -> ( `' ( x e. A |-> B ) " ( y (,) +oo ) ) e. dom vol )
122 simplr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> 0 < y )
123 0red 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> 0 e. RR )
124 1 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> B e. RR )
125 simpllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> y e. RR )
126 maxlt 
 |-  ( ( 0 e. RR /\ B e. RR /\ y e. RR ) -> ( if ( 0 <_ B , B , 0 ) < y <-> ( 0 < y /\ B < y ) ) )
127 123 124 125 126 syl3anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) < y <-> ( 0 < y /\ B < y ) ) )
128 122 127 mpbirand 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) < y <-> B < y ) )
129 7 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
130 129 biantrurd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) < y <-> ( if ( 0 <_ B , B , 0 ) e. RR /\ if ( 0 <_ B , B , 0 ) < y ) ) )
131 124 biantrurd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> ( B < y <-> ( B e. RR /\ B < y ) ) )
132 128 130 131 3bitr3d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> ( ( if ( 0 <_ B , B , 0 ) e. RR /\ if ( 0 <_ B , B , 0 ) < y ) <-> ( B e. RR /\ B < y ) ) )
133 125 rexrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> y e. RR* )
134 elioomnf 
 |-  ( y e. RR* -> ( if ( 0 <_ B , B , 0 ) e. ( -oo (,) y ) <-> ( if ( 0 <_ B , B , 0 ) e. RR /\ if ( 0 <_ B , B , 0 ) < y ) ) )
135 133 134 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) e. ( -oo (,) y ) <-> ( if ( 0 <_ B , B , 0 ) e. RR /\ if ( 0 <_ B , B , 0 ) < y ) ) )
136 elioomnf 
 |-  ( y e. RR* -> ( B e. ( -oo (,) y ) <-> ( B e. RR /\ B < y ) ) )
137 133 136 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> ( B e. ( -oo (,) y ) <-> ( B e. RR /\ B < y ) ) )
138 132 135 137 3bitr4d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) e. ( -oo (,) y ) <-> B e. ( -oo (,) y ) ) )
139 96 eleq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( -oo (,) y ) <-> if ( 0 <_ B , B , 0 ) e. ( -oo (,) y ) ) )
140 139 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> ( ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( -oo (,) y ) <-> if ( 0 <_ B , B , 0 ) e. ( -oo (,) y ) ) )
141 44 eleq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) e. ( -oo (,) y ) <-> B e. ( -oo (,) y ) ) )
142 141 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) e. ( -oo (,) y ) <-> B e. ( -oo (,) y ) ) )
143 138 140 142 3bitr4d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ 0 < y ) /\ x e. A ) -> ( ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( -oo (,) y ) <-> ( ( x e. A |-> B ) ` x ) e. ( -oo (,) y ) ) )
144 143 pm5.32da 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 < y ) -> ( ( x e. A /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( -oo (,) y ) ) <-> ( x e. A /\ ( ( x e. A |-> B ) ` x ) e. ( -oo (,) y ) ) ) )
145 elpreima 
 |-  ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) Fn A -> ( x e. ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( -oo (,) y ) ) <-> ( x e. A /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( -oo (,) y ) ) ) )
146 102 103 145 3syl 
 |-  ( ph -> ( x e. ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( -oo (,) y ) ) <-> ( x e. A /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( -oo (,) y ) ) ) )
147 146 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 < y ) -> ( x e. ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( -oo (,) y ) ) <-> ( x e. A /\ ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ` x ) e. ( -oo (,) y ) ) ) )
148 elpreima 
 |-  ( ( x e. A |-> B ) Fn A -> ( x e. ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) <-> ( x e. A /\ ( ( x e. A |-> B ) ` x ) e. ( -oo (,) y ) ) ) )
149 4 54 148 3syl 
 |-  ( ph -> ( x e. ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) <-> ( x e. A /\ ( ( x e. A |-> B ) ` x ) e. ( -oo (,) y ) ) ) )
150 149 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 < y ) -> ( x e. ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) <-> ( x e. A /\ ( ( x e. A |-> B ) ` x ) e. ( -oo (,) y ) ) ) )
151 144 147 150 3bitr4d 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 < y ) -> ( x e. ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( -oo (,) y ) ) <-> x e. ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) ) )
152 151 alrimiv 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 < y ) -> A. x ( x e. ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( -oo (,) y ) ) <-> x e. ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) ) )
153 nfcv 
 |-  F/_ x ( -oo (,) y )
154 111 153 nfima 
 |-  F/_ x ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( -oo (,) y ) )
155 65 153 nfima 
 |-  F/_ x ( `' ( x e. A |-> B ) " ( -oo (,) y ) )
156 154 155 cleqf 
 |-  ( ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( -oo (,) y ) ) = ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) <-> A. x ( x e. ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( -oo (,) y ) ) <-> x e. ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) ) )
157 152 156 sylibr 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 < y ) -> ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( -oo (,) y ) ) = ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) )
158 mbfima 
 |-  ( ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ B , B , 0 ) ) : A --> RR ) -> ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( -oo (,) y ) ) e. dom vol )
159 2 102 158 syl2anc 
 |-  ( ph -> ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( -oo (,) y ) ) e. dom vol )
160 159 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 < y ) -> ( `' ( x e. A |-> if ( 0 <_ B , B , 0 ) ) " ( -oo (,) y ) ) e. dom vol )
161 157 160 eqeltrrd 
 |-  ( ( ( ph /\ y e. RR ) /\ 0 < y ) -> ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) e. dom vol )
162 simplr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> y <_ 0 )
163 simpllr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> y e. RR )
164 163 le0neg1d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( y <_ 0 <-> 0 <_ -u y ) )
165 162 164 mpbid 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> 0 <_ -u y )
166 165 biantrurd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( -u B <_ -u y <-> ( 0 <_ -u y /\ -u B <_ -u y ) ) )
167 1 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> B e. RR )
168 163 167 lenegd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( y <_ B <-> -u B <_ -u y ) )
169 0red 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> 0 e. RR )
170 167 renegcld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> -u B e. RR )
171 163 renegcld 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> -u y e. RR )
172 maxle 
 |-  ( ( 0 e. RR /\ -u B e. RR /\ -u y e. RR ) -> ( if ( 0 <_ -u B , -u B , 0 ) <_ -u y <-> ( 0 <_ -u y /\ -u B <_ -u y ) ) )
173 169 170 171 172 syl3anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) <_ -u y <-> ( 0 <_ -u y /\ -u B <_ -u y ) ) )
174 166 168 173 3bitr4rd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) <_ -u y <-> y <_ B ) )
175 174 notbid 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( -. if ( 0 <_ -u B , -u B , 0 ) <_ -u y <-> -. y <_ B ) )
176 24 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
177 171 176 ltnled 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( -u y < if ( 0 <_ -u B , -u B , 0 ) <-> -. if ( 0 <_ -u B , -u B , 0 ) <_ -u y ) )
178 167 163 ltnled 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( B < y <-> -. y <_ B ) )
179 175 177 178 3bitr4d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( -u y < if ( 0 <_ -u B , -u B , 0 ) <-> B < y ) )
180 176 biantrurd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( -u y < if ( 0 <_ -u B , -u B , 0 ) <-> ( if ( 0 <_ -u B , -u B , 0 ) e. RR /\ -u y < if ( 0 <_ -u B , -u B , 0 ) ) ) )
181 167 biantrurd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( B < y <-> ( B e. RR /\ B < y ) ) )
182 179 180 181 3bitr3d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( ( if ( 0 <_ -u B , -u B , 0 ) e. RR /\ -u y < if ( 0 <_ -u B , -u B , 0 ) ) <-> ( B e. RR /\ B < y ) ) )
183 171 rexrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> -u y e. RR* )
184 elioopnf 
 |-  ( -u y e. RR* -> ( if ( 0 <_ -u B , -u B , 0 ) e. ( -u y (,) +oo ) <-> ( if ( 0 <_ -u B , -u B , 0 ) e. RR /\ -u y < if ( 0 <_ -u B , -u B , 0 ) ) ) )
185 183 184 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) e. ( -u y (,) +oo ) <-> ( if ( 0 <_ -u B , -u B , 0 ) e. RR /\ -u y < if ( 0 <_ -u B , -u B , 0 ) ) ) )
186 163 rexrd 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> y e. RR* )
187 186 136 syl 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( B e. ( -oo (,) y ) <-> ( B e. RR /\ B < y ) ) )
188 182 185 187 3bitr4d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) e. ( -u y (,) +oo ) <-> B e. ( -oo (,) y ) ) )
189 39 eleq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -u y (,) +oo ) <-> if ( 0 <_ -u B , -u B , 0 ) e. ( -u y (,) +oo ) ) )
190 189 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -u y (,) +oo ) <-> if ( 0 <_ -u B , -u B , 0 ) e. ( -u y (,) +oo ) ) )
191 141 ad4ant14 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( ( ( x e. A |-> B ) ` x ) e. ( -oo (,) y ) <-> B e. ( -oo (,) y ) ) )
192 188 190 191 3bitr4d 
 |-  ( ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) /\ x e. A ) -> ( ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -u y (,) +oo ) <-> ( ( x e. A |-> B ) ` x ) e. ( -oo (,) y ) ) )
193 192 pm5.32da 
 |-  ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) -> ( ( x e. A /\ ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -u y (,) +oo ) ) <-> ( x e. A /\ ( ( x e. A |-> B ) ` x ) e. ( -oo (,) y ) ) ) )
194 elpreima 
 |-  ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) Fn A -> ( x e. ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -u y (,) +oo ) ) <-> ( x e. A /\ ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -u y (,) +oo ) ) ) )
195 49 50 194 3syl 
 |-  ( ph -> ( x e. ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -u y (,) +oo ) ) <-> ( x e. A /\ ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -u y (,) +oo ) ) ) )
196 195 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) -> ( x e. ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -u y (,) +oo ) ) <-> ( x e. A /\ ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ` x ) e. ( -u y (,) +oo ) ) ) )
197 149 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) -> ( x e. ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) <-> ( x e. A /\ ( ( x e. A |-> B ) ` x ) e. ( -oo (,) y ) ) ) )
198 193 196 197 3bitr4d 
 |-  ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) -> ( x e. ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -u y (,) +oo ) ) <-> x e. ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) ) )
199 198 alrimiv 
 |-  ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) -> A. x ( x e. ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -u y (,) +oo ) ) <-> x e. ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) ) )
200 nfcv 
 |-  F/_ x ( -u y (,) +oo )
201 61 200 nfima 
 |-  F/_ x ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -u y (,) +oo ) )
202 201 155 cleqf 
 |-  ( ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -u y (,) +oo ) ) = ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) <-> A. x ( x e. ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -u y (,) +oo ) ) <-> x e. ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) ) )
203 199 202 sylibr 
 |-  ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) -> ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -u y (,) +oo ) ) = ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) )
204 mbfima 
 |-  ( ( ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) : A --> RR ) -> ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -u y (,) +oo ) ) e. dom vol )
205 3 49 204 syl2anc 
 |-  ( ph -> ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -u y (,) +oo ) ) e. dom vol )
206 205 ad2antrr 
 |-  ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) -> ( `' ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) " ( -u y (,) +oo ) ) e. dom vol )
207 203 206 eqeltrrd 
 |-  ( ( ( ph /\ y e. RR ) /\ y <_ 0 ) -> ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) e. dom vol )
208 161 207 120 119 ltlecasei 
 |-  ( ( ph /\ y e. RR ) -> ( `' ( x e. A |-> B ) " ( -oo (,) y ) ) e. dom vol )
209 4 8 121 208 ismbf2d 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )