Metamath Proof Explorer

Theorem mbfmax

Description: The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses mbfmax.1 
|- ( ph -> F : A --> RR )
mbfmax.2 
|- ( ph -> F e. MblFn )
mbfmax.3 
|- ( ph -> G : A --> RR )
mbfmax.4 
|- ( ph -> G e. MblFn )
mbfmax.5 
|- H = ( x e. A |-> if ( ( F ` x ) <_ ( G ` x ) , ( G ` x ) , ( F ` x ) ) )
Assertion mbfmax 
|- ( ph -> H e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfmax.1 
 |-  ( ph -> F : A --> RR )
2 mbfmax.2 
 |-  ( ph -> F e. MblFn )
3 mbfmax.3 
 |-  ( ph -> G : A --> RR )
4 mbfmax.4 
 |-  ( ph -> G e. MblFn )
5 mbfmax.5 
 |-  H = ( x e. A |-> if ( ( F ` x ) <_ ( G ` x ) , ( G ` x ) , ( F ` x ) ) )
6 3 ffvelcdmda 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) e. RR )
7 1 ffvelcdmda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. RR )
8 6 7 ifcld 
 |-  ( ( ph /\ x e. A ) -> if ( ( F ` x ) <_ ( G ` x ) , ( G ` x ) , ( F ` x ) ) e. RR )
9 8 5 fmptd 
 |-  ( ph -> H : A --> RR )
10 1 adantr 
 |-  ( ( ph /\ y e. RR* ) -> F : A --> RR )
11 10 ffvelcdmda 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( F ` z ) e. RR )
12 11 rexrd 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( F ` z ) e. RR* )
13 3 adantr 
 |-  ( ( ph /\ y e. RR* ) -> G : A --> RR )
14 13 ffvelcdmda 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( G ` z ) e. RR )
15 14 rexrd 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( G ` z ) e. RR* )
16 simplr 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> y e. RR* )
17 xrmaxle 
 |-  ( ( ( F ` z ) e. RR* /\ ( G ` z ) e. RR* /\ y e. RR* ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) <_ y <-> ( ( F ` z ) <_ y /\ ( G ` z ) <_ y ) ) )
18 12 15 16 17 syl3anc 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) <_ y <-> ( ( F ` z ) <_ y /\ ( G ` z ) <_ y ) ) )
19 18 notbid 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( -. if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) <_ y <-> -. ( ( F ` z ) <_ y /\ ( G ` z ) <_ y ) ) )
20 ianor 
 |-  ( -. ( ( F ` z ) <_ y /\ ( G ` z ) <_ y ) <-> ( -. ( F ` z ) <_ y \/ -. ( G ` z ) <_ y ) )
21 19 20 bitrdi 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( -. if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) <_ y <-> ( -. ( F ` z ) <_ y \/ -. ( G ` z ) <_ y ) ) )
22 pnfxr 
 |-  +oo e. RR*
23 elioo2 
 |-  ( ( y e. RR* /\ +oo e. RR* ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. ( y (,) +oo ) <-> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ y < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < +oo ) ) )
24 16 22 23 sylancl 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. ( y (,) +oo ) <-> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ y < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < +oo ) ) )
25 3anan12 
 |-  ( ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ y < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < +oo ) <-> ( y < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) /\ ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < +oo ) ) )
26 24 25 bitrdi 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. ( y (,) +oo ) <-> ( y < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) /\ ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < +oo ) ) ) )
27 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
28 fveq2 
 |-  ( x = z -> ( G ` x ) = ( G ` z ) )
29 27 28 breq12d 
 |-  ( x = z -> ( ( F ` x ) <_ ( G ` x ) <-> ( F ` z ) <_ ( G ` z ) ) )
30 29 28 27 ifbieq12d 
 |-  ( x = z -> if ( ( F ` x ) <_ ( G ` x ) , ( G ` x ) , ( F ` x ) ) = if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) )
31 fvex 
 |-  ( G ` z ) e. _V
32 fvex 
 |-  ( F ` z ) e. _V
33 31 32 ifex 
 |-  if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. _V
34 30 5 33 fvmpt 
 |-  ( z e. A -> ( H ` z ) = if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) )
35 34 adantl 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( H ` z ) = if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) )
36 35 eleq1d 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( H ` z ) e. ( y (,) +oo ) <-> if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. ( y (,) +oo ) ) )
37 14 11 ifcld 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR )
38 ltpnf 
 |-  ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR -> if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < +oo )
39 37 38 jccir 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < +oo ) )
40 39 biantrud 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( y < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) <-> ( y < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) /\ ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < +oo ) ) ) )
41 26 36 40 3bitr4d 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( H ` z ) e. ( y (,) +oo ) <-> y < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) ) )
42 37 rexrd 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR* )
43 xrltnle 
 |-  ( ( y e. RR* /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR* ) -> ( y < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) <-> -. if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) <_ y ) )
44 16 42 43 syl2anc 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( y < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) <-> -. if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) <_ y ) )
45 41 44 bitrd 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( H ` z ) e. ( y (,) +oo ) <-> -. if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) <_ y ) )
46 elioo2 
 |-  ( ( y e. RR* /\ +oo e. RR* ) -> ( ( F ` z ) e. ( y (,) +oo ) <-> ( ( F ` z ) e. RR /\ y < ( F ` z ) /\ ( F ` z ) < +oo ) ) )
47 16 22 46 sylancl 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( F ` z ) e. ( y (,) +oo ) <-> ( ( F ` z ) e. RR /\ y < ( F ` z ) /\ ( F ` z ) < +oo ) ) )
48 3anan12 
 |-  ( ( ( F ` z ) e. RR /\ y < ( F ` z ) /\ ( F ` z ) < +oo ) <-> ( y < ( F ` z ) /\ ( ( F ` z ) e. RR /\ ( F ` z ) < +oo ) ) )
49 47 48 bitrdi 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( F ` z ) e. ( y (,) +oo ) <-> ( y < ( F ` z ) /\ ( ( F ` z ) e. RR /\ ( F ` z ) < +oo ) ) ) )
50 ltpnf 
 |-  ( ( F ` z ) e. RR -> ( F ` z ) < +oo )
51 11 50 jccir 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( F ` z ) e. RR /\ ( F ` z ) < +oo ) )
52 51 biantrud 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( y < ( F ` z ) <-> ( y < ( F ` z ) /\ ( ( F ` z ) e. RR /\ ( F ` z ) < +oo ) ) ) )
53 xrltnle 
 |-  ( ( y e. RR* /\ ( F ` z ) e. RR* ) -> ( y < ( F ` z ) <-> -. ( F ` z ) <_ y ) )
54 16 12 53 syl2anc 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( y < ( F ` z ) <-> -. ( F ` z ) <_ y ) )
55 49 52 54 3bitr2d 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( F ` z ) e. ( y (,) +oo ) <-> -. ( F ` z ) <_ y ) )
56 elioo2 
 |-  ( ( y e. RR* /\ +oo e. RR* ) -> ( ( G ` z ) e. ( y (,) +oo ) <-> ( ( G ` z ) e. RR /\ y < ( G ` z ) /\ ( G ` z ) < +oo ) ) )
57 16 22 56 sylancl 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( G ` z ) e. ( y (,) +oo ) <-> ( ( G ` z ) e. RR /\ y < ( G ` z ) /\ ( G ` z ) < +oo ) ) )
58 3anan12 
 |-  ( ( ( G ` z ) e. RR /\ y < ( G ` z ) /\ ( G ` z ) < +oo ) <-> ( y < ( G ` z ) /\ ( ( G ` z ) e. RR /\ ( G ` z ) < +oo ) ) )
59 57 58 bitrdi 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( G ` z ) e. ( y (,) +oo ) <-> ( y < ( G ` z ) /\ ( ( G ` z ) e. RR /\ ( G ` z ) < +oo ) ) ) )
60 ltpnf 
 |-  ( ( G ` z ) e. RR -> ( G ` z ) < +oo )
61 14 60 jccir 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( G ` z ) e. RR /\ ( G ` z ) < +oo ) )
62 61 biantrud 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( y < ( G ` z ) <-> ( y < ( G ` z ) /\ ( ( G ` z ) e. RR /\ ( G ` z ) < +oo ) ) ) )
63 xrltnle 
 |-  ( ( y e. RR* /\ ( G ` z ) e. RR* ) -> ( y < ( G ` z ) <-> -. ( G ` z ) <_ y ) )
64 16 15 63 syl2anc 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( y < ( G ` z ) <-> -. ( G ` z ) <_ y ) )
65 59 62 64 3bitr2d 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( G ` z ) e. ( y (,) +oo ) <-> -. ( G ` z ) <_ y ) )
66 55 65 orbi12d 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( ( F ` z ) e. ( y (,) +oo ) \/ ( G ` z ) e. ( y (,) +oo ) ) <-> ( -. ( F ` z ) <_ y \/ -. ( G ` z ) <_ y ) ) )
67 21 45 66 3bitr4d 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( H ` z ) e. ( y (,) +oo ) <-> ( ( F ` z ) e. ( y (,) +oo ) \/ ( G ` z ) e. ( y (,) +oo ) ) ) )
68 67 pm5.32da 
 |-  ( ( ph /\ y e. RR* ) -> ( ( z e. A /\ ( H ` z ) e. ( y (,) +oo ) ) <-> ( z e. A /\ ( ( F ` z ) e. ( y (,) +oo ) \/ ( G ` z ) e. ( y (,) +oo ) ) ) ) )
69 andi 
 |-  ( ( z e. A /\ ( ( F ` z ) e. ( y (,) +oo ) \/ ( G ` z ) e. ( y (,) +oo ) ) ) <-> ( ( z e. A /\ ( F ` z ) e. ( y (,) +oo ) ) \/ ( z e. A /\ ( G ` z ) e. ( y (,) +oo ) ) ) )
70 68 69 bitrdi 
 |-  ( ( ph /\ y e. RR* ) -> ( ( z e. A /\ ( H ` z ) e. ( y (,) +oo ) ) <-> ( ( z e. A /\ ( F ` z ) e. ( y (,) +oo ) ) \/ ( z e. A /\ ( G ` z ) e. ( y (,) +oo ) ) ) ) )
71 9 ffnd 
 |-  ( ph -> H Fn A )
72 71 adantr 
 |-  ( ( ph /\ y e. RR* ) -> H Fn A )
73 elpreima 
 |-  ( H Fn A -> ( z e. ( `' H " ( y (,) +oo ) ) <-> ( z e. A /\ ( H ` z ) e. ( y (,) +oo ) ) ) )
74 72 73 syl 
 |-  ( ( ph /\ y e. RR* ) -> ( z e. ( `' H " ( y (,) +oo ) ) <-> ( z e. A /\ ( H ` z ) e. ( y (,) +oo ) ) ) )
75 10 ffnd 
 |-  ( ( ph /\ y e. RR* ) -> F Fn A )
76 elpreima 
 |-  ( F Fn A -> ( z e. ( `' F " ( y (,) +oo ) ) <-> ( z e. A /\ ( F ` z ) e. ( y (,) +oo ) ) ) )
77 75 76 syl 
 |-  ( ( ph /\ y e. RR* ) -> ( z e. ( `' F " ( y (,) +oo ) ) <-> ( z e. A /\ ( F ` z ) e. ( y (,) +oo ) ) ) )
78 13 ffnd 
 |-  ( ( ph /\ y e. RR* ) -> G Fn A )
79 elpreima 
 |-  ( G Fn A -> ( z e. ( `' G " ( y (,) +oo ) ) <-> ( z e. A /\ ( G ` z ) e. ( y (,) +oo ) ) ) )
80 78 79 syl 
 |-  ( ( ph /\ y e. RR* ) -> ( z e. ( `' G " ( y (,) +oo ) ) <-> ( z e. A /\ ( G ` z ) e. ( y (,) +oo ) ) ) )
81 77 80 orbi12d 
 |-  ( ( ph /\ y e. RR* ) -> ( ( z e. ( `' F " ( y (,) +oo ) ) \/ z e. ( `' G " ( y (,) +oo ) ) ) <-> ( ( z e. A /\ ( F ` z ) e. ( y (,) +oo ) ) \/ ( z e. A /\ ( G ` z ) e. ( y (,) +oo ) ) ) ) )
82 70 74 81 3bitr4d 
 |-  ( ( ph /\ y e. RR* ) -> ( z e. ( `' H " ( y (,) +oo ) ) <-> ( z e. ( `' F " ( y (,) +oo ) ) \/ z e. ( `' G " ( y (,) +oo ) ) ) ) )
83 elun 
 |-  ( z e. ( ( `' F " ( y (,) +oo ) ) u. ( `' G " ( y (,) +oo ) ) ) <-> ( z e. ( `' F " ( y (,) +oo ) ) \/ z e. ( `' G " ( y (,) +oo ) ) ) )
84 82 83 bitr4di 
 |-  ( ( ph /\ y e. RR* ) -> ( z e. ( `' H " ( y (,) +oo ) ) <-> z e. ( ( `' F " ( y (,) +oo ) ) u. ( `' G " ( y (,) +oo ) ) ) ) )
85 84 eqrdv 
 |-  ( ( ph /\ y e. RR* ) -> ( `' H " ( y (,) +oo ) ) = ( ( `' F " ( y (,) +oo ) ) u. ( `' G " ( y (,) +oo ) ) ) )
86 mbfima 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( y (,) +oo ) ) e. dom vol )
87 2 1 86 syl2anc 
 |-  ( ph -> ( `' F " ( y (,) +oo ) ) e. dom vol )
88 mbfima 
 |-  ( ( G e. MblFn /\ G : A --> RR ) -> ( `' G " ( y (,) +oo ) ) e. dom vol )
89 4 3 88 syl2anc 
 |-  ( ph -> ( `' G " ( y (,) +oo ) ) e. dom vol )
90 unmbl 
 |-  ( ( ( `' F " ( y (,) +oo ) ) e. dom vol /\ ( `' G " ( y (,) +oo ) ) e. dom vol ) -> ( ( `' F " ( y (,) +oo ) ) u. ( `' G " ( y (,) +oo ) ) ) e. dom vol )
91 87 89 90 syl2anc 
 |-  ( ph -> ( ( `' F " ( y (,) +oo ) ) u. ( `' G " ( y (,) +oo ) ) ) e. dom vol )
92 91 adantr 
 |-  ( ( ph /\ y e. RR* ) -> ( ( `' F " ( y (,) +oo ) ) u. ( `' G " ( y (,) +oo ) ) ) e. dom vol )
93 85 92 eqeltrd 
 |-  ( ( ph /\ y e. RR* ) -> ( `' H " ( y (,) +oo ) ) e. dom vol )
94 xrmaxlt 
 |-  ( ( ( F ` z ) e. RR* /\ ( G ` z ) e. RR* /\ y e. RR* ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < y <-> ( ( F ` z ) < y /\ ( G ` z ) < y ) ) )
95 12 15 16 94 syl3anc 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < y <-> ( ( F ` z ) < y /\ ( G ` z ) < y ) ) )
96 mnfxr 
 |-  -oo e. RR*
97 elioo2 
 |-  ( ( -oo e. RR* /\ y e. RR* ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. ( -oo (,) y ) <-> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ -oo < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < y ) ) )
98 96 16 97 sylancr 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. ( -oo (,) y ) <-> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ -oo < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < y ) ) )
99 df-3an 
 |-  ( ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ -oo < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < y ) <-> ( ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ -oo < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) ) /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < y ) )
100 98 99 bitrdi 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. ( -oo (,) y ) <-> ( ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ -oo < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) ) /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < y ) ) )
101 35 eleq1d 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( H ` z ) e. ( -oo (,) y ) <-> if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. ( -oo (,) y ) ) )
102 mnflt 
 |-  ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR -> -oo < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) )
103 37 102 jccir 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ -oo < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) ) )
104 103 biantrurd 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < y <-> ( ( if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) e. RR /\ -oo < if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) ) /\ if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < y ) ) )
105 100 101 104 3bitr4d 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( H ` z ) e. ( -oo (,) y ) <-> if ( ( F ` z ) <_ ( G ` z ) , ( G ` z ) , ( F ` z ) ) < y ) )
106 mnflt 
 |-  ( ( F ` z ) e. RR -> -oo < ( F ` z ) )
107 11 106 jccir 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( F ` z ) e. RR /\ -oo < ( F ` z ) ) )
108 elioo2 
 |-  ( ( -oo e. RR* /\ y e. RR* ) -> ( ( F ` z ) e. ( -oo (,) y ) <-> ( ( F ` z ) e. RR /\ -oo < ( F ` z ) /\ ( F ` z ) < y ) ) )
109 96 16 108 sylancr 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( F ` z ) e. ( -oo (,) y ) <-> ( ( F ` z ) e. RR /\ -oo < ( F ` z ) /\ ( F ` z ) < y ) ) )
110 df-3an 
 |-  ( ( ( F ` z ) e. RR /\ -oo < ( F ` z ) /\ ( F ` z ) < y ) <-> ( ( ( F ` z ) e. RR /\ -oo < ( F ` z ) ) /\ ( F ` z ) < y ) )
111 109 110 bitrdi 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( F ` z ) e. ( -oo (,) y ) <-> ( ( ( F ` z ) e. RR /\ -oo < ( F ` z ) ) /\ ( F ` z ) < y ) ) )
112 107 111 mpbirand 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( F ` z ) e. ( -oo (,) y ) <-> ( F ` z ) < y ) )
113 mnflt 
 |-  ( ( G ` z ) e. RR -> -oo < ( G ` z ) )
114 14 113 jccir 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( G ` z ) e. RR /\ -oo < ( G ` z ) ) )
115 elioo2 
 |-  ( ( -oo e. RR* /\ y e. RR* ) -> ( ( G ` z ) e. ( -oo (,) y ) <-> ( ( G ` z ) e. RR /\ -oo < ( G ` z ) /\ ( G ` z ) < y ) ) )
116 96 16 115 sylancr 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( G ` z ) e. ( -oo (,) y ) <-> ( ( G ` z ) e. RR /\ -oo < ( G ` z ) /\ ( G ` z ) < y ) ) )
117 df-3an 
 |-  ( ( ( G ` z ) e. RR /\ -oo < ( G ` z ) /\ ( G ` z ) < y ) <-> ( ( ( G ` z ) e. RR /\ -oo < ( G ` z ) ) /\ ( G ` z ) < y ) )
118 116 117 bitrdi 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( G ` z ) e. ( -oo (,) y ) <-> ( ( ( G ` z ) e. RR /\ -oo < ( G ` z ) ) /\ ( G ` z ) < y ) ) )
119 114 118 mpbirand 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( G ` z ) e. ( -oo (,) y ) <-> ( G ` z ) < y ) )
120 112 119 anbi12d 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( ( F ` z ) e. ( -oo (,) y ) /\ ( G ` z ) e. ( -oo (,) y ) ) <-> ( ( F ` z ) < y /\ ( G ` z ) < y ) ) )
121 95 105 120 3bitr4d 
 |-  ( ( ( ph /\ y e. RR* ) /\ z e. A ) -> ( ( H ` z ) e. ( -oo (,) y ) <-> ( ( F ` z ) e. ( -oo (,) y ) /\ ( G ` z ) e. ( -oo (,) y ) ) ) )
122 121 pm5.32da 
 |-  ( ( ph /\ y e. RR* ) -> ( ( z e. A /\ ( H ` z ) e. ( -oo (,) y ) ) <-> ( z e. A /\ ( ( F ` z ) e. ( -oo (,) y ) /\ ( G ` z ) e. ( -oo (,) y ) ) ) ) )
123 anandi 
 |-  ( ( z e. A /\ ( ( F ` z ) e. ( -oo (,) y ) /\ ( G ` z ) e. ( -oo (,) y ) ) ) <-> ( ( z e. A /\ ( F ` z ) e. ( -oo (,) y ) ) /\ ( z e. A /\ ( G ` z ) e. ( -oo (,) y ) ) ) )
124 122 123 bitrdi 
 |-  ( ( ph /\ y e. RR* ) -> ( ( z e. A /\ ( H ` z ) e. ( -oo (,) y ) ) <-> ( ( z e. A /\ ( F ` z ) e. ( -oo (,) y ) ) /\ ( z e. A /\ ( G ` z ) e. ( -oo (,) y ) ) ) ) )
125 elpreima 
 |-  ( H Fn A -> ( z e. ( `' H " ( -oo (,) y ) ) <-> ( z e. A /\ ( H ` z ) e. ( -oo (,) y ) ) ) )
126 72 125 syl 
 |-  ( ( ph /\ y e. RR* ) -> ( z e. ( `' H " ( -oo (,) y ) ) <-> ( z e. A /\ ( H ` z ) e. ( -oo (,) y ) ) ) )
127 elpreima 
 |-  ( F Fn A -> ( z e. ( `' F " ( -oo (,) y ) ) <-> ( z e. A /\ ( F ` z ) e. ( -oo (,) y ) ) ) )
128 75 127 syl 
 |-  ( ( ph /\ y e. RR* ) -> ( z e. ( `' F " ( -oo (,) y ) ) <-> ( z e. A /\ ( F ` z ) e. ( -oo (,) y ) ) ) )
129 elpreima 
 |-  ( G Fn A -> ( z e. ( `' G " ( -oo (,) y ) ) <-> ( z e. A /\ ( G ` z ) e. ( -oo (,) y ) ) ) )
130 78 129 syl 
 |-  ( ( ph /\ y e. RR* ) -> ( z e. ( `' G " ( -oo (,) y ) ) <-> ( z e. A /\ ( G ` z ) e. ( -oo (,) y ) ) ) )
131 128 130 anbi12d 
 |-  ( ( ph /\ y e. RR* ) -> ( ( z e. ( `' F " ( -oo (,) y ) ) /\ z e. ( `' G " ( -oo (,) y ) ) ) <-> ( ( z e. A /\ ( F ` z ) e. ( -oo (,) y ) ) /\ ( z e. A /\ ( G ` z ) e. ( -oo (,) y ) ) ) ) )
132 124 126 131 3bitr4d 
 |-  ( ( ph /\ y e. RR* ) -> ( z e. ( `' H " ( -oo (,) y ) ) <-> ( z e. ( `' F " ( -oo (,) y ) ) /\ z e. ( `' G " ( -oo (,) y ) ) ) ) )
133 elin 
 |-  ( z e. ( ( `' F " ( -oo (,) y ) ) i^i ( `' G " ( -oo (,) y ) ) ) <-> ( z e. ( `' F " ( -oo (,) y ) ) /\ z e. ( `' G " ( -oo (,) y ) ) ) )
134 132 133 bitr4di 
 |-  ( ( ph /\ y e. RR* ) -> ( z e. ( `' H " ( -oo (,) y ) ) <-> z e. ( ( `' F " ( -oo (,) y ) ) i^i ( `' G " ( -oo (,) y ) ) ) ) )
135 134 eqrdv 
 |-  ( ( ph /\ y e. RR* ) -> ( `' H " ( -oo (,) y ) ) = ( ( `' F " ( -oo (,) y ) ) i^i ( `' G " ( -oo (,) y ) ) ) )
136 mbfima 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( -oo (,) y ) ) e. dom vol )
137 2 1 136 syl2anc 
 |-  ( ph -> ( `' F " ( -oo (,) y ) ) e. dom vol )
138 mbfima 
 |-  ( ( G e. MblFn /\ G : A --> RR ) -> ( `' G " ( -oo (,) y ) ) e. dom vol )
139 4 3 138 syl2anc 
 |-  ( ph -> ( `' G " ( -oo (,) y ) ) e. dom vol )
140 inmbl 
 |-  ( ( ( `' F " ( -oo (,) y ) ) e. dom vol /\ ( `' G " ( -oo (,) y ) ) e. dom vol ) -> ( ( `' F " ( -oo (,) y ) ) i^i ( `' G " ( -oo (,) y ) ) ) e. dom vol )
141 137 139 140 syl2anc 
 |-  ( ph -> ( ( `' F " ( -oo (,) y ) ) i^i ( `' G " ( -oo (,) y ) ) ) e. dom vol )
142 141 adantr 
 |-  ( ( ph /\ y e. RR* ) -> ( ( `' F " ( -oo (,) y ) ) i^i ( `' G " ( -oo (,) y ) ) ) e. dom vol )
143 135 142 eqeltrd 
 |-  ( ( ph /\ y e. RR* ) -> ( `' H " ( -oo (,) y ) ) e. dom vol )
144 9 93 143 ismbfd 
 |-  ( ph -> H e. MblFn )