Metamath Proof Explorer

Theorem mbfsup

Description: The supremum of a sequence of measurable, real-valued functions is measurable. Note that in this and related theorems, B ( n , x ) is a function of both n and x , since it is an n -indexed sequence of functions on x . (Contributed by Mario Carneiro, 14-Aug-2014) (Revised by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses mbfsup.1 
|- Z = ( ZZ>= ` M )
mbfsup.2 
|- G = ( x e. A |-> sup ( ran ( n e. Z |-> B ) , RR , < ) )
mbfsup.3 
|- ( ph -> M e. ZZ )
mbfsup.4 
|- ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )
mbfsup.5 
|- ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )
mbfsup.6 
|- ( ( ph /\ x e. A ) -> E. y e. RR A. n e. Z B <_ y )
Assertion mbfsup 
|- ( ph -> G e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfsup.1 
 |-  Z = ( ZZ>= ` M )
2 mbfsup.2 
 |-  G = ( x e. A |-> sup ( ran ( n e. Z |-> B ) , RR , < ) )
3 mbfsup.3 
 |-  ( ph -> M e. ZZ )
4 mbfsup.4 
 |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) e. MblFn )
5 mbfsup.5 
 |-  ( ( ph /\ ( n e. Z /\ x e. A ) ) -> B e. RR )
6 mbfsup.6 
 |-  ( ( ph /\ x e. A ) -> E. y e. RR A. n e. Z B <_ y )
7 5 anassrs 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. A ) -> B e. RR )
8 7 an32s 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> B e. RR )
9 8 fmpttd 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) : Z --> RR )
10 9 frnd 
 |-  ( ( ph /\ x e. A ) -> ran ( n e. Z |-> B ) C_ RR )
11 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
12 3 11 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
13 12 1 eleqtrrdi 
 |-  ( ph -> M e. Z )
14 13 adantr 
 |-  ( ( ph /\ x e. A ) -> M e. Z )
15 eqid 
 |-  ( n e. Z |-> B ) = ( n e. Z |-> B )
16 15 8 dmmptd 
 |-  ( ( ph /\ x e. A ) -> dom ( n e. Z |-> B ) = Z )
17 14 16 eleqtrrd 
 |-  ( ( ph /\ x e. A ) -> M e. dom ( n e. Z |-> B ) )
18 17 ne0d 
 |-  ( ( ph /\ x e. A ) -> dom ( n e. Z |-> B ) =/= (/) )
19 dm0rn0 
 |-  ( dom ( n e. Z |-> B ) = (/) <-> ran ( n e. Z |-> B ) = (/) )
20 19 necon3bii 
 |-  ( dom ( n e. Z |-> B ) =/= (/) <-> ran ( n e. Z |-> B ) =/= (/) )
21 18 20 sylib 
 |-  ( ( ph /\ x e. A ) -> ran ( n e. Z |-> B ) =/= (/) )
22 9 ffnd 
 |-  ( ( ph /\ x e. A ) -> ( n e. Z |-> B ) Fn Z )
23 breq1 
 |-  ( z = ( ( n e. Z |-> B ) ` m ) -> ( z <_ y <-> ( ( n e. Z |-> B ) ` m ) <_ y ) )
24 23 ralrn 
 |-  ( ( n e. Z |-> B ) Fn Z -> ( A. z e. ran ( n e. Z |-> B ) z <_ y <-> A. m e. Z ( ( n e. Z |-> B ) ` m ) <_ y ) )
25 22 24 syl 
 |-  ( ( ph /\ x e. A ) -> ( A. z e. ran ( n e. Z |-> B ) z <_ y <-> A. m e. Z ( ( n e. Z |-> B ) ` m ) <_ y ) )
26 nffvmpt1 
 |-  F/_ n ( ( n e. Z |-> B ) ` m )
27 nfcv 
 |-  F/_ n <_
28 nfcv 
 |-  F/_ n y
29 26 27 28 nfbr 
 |-  F/ n ( ( n e. Z |-> B ) ` m ) <_ y
30 nfv 
 |-  F/ m ( ( n e. Z |-> B ) ` n ) <_ y
31 fveq2 
 |-  ( m = n -> ( ( n e. Z |-> B ) ` m ) = ( ( n e. Z |-> B ) ` n ) )
32 31 breq1d 
 |-  ( m = n -> ( ( ( n e. Z |-> B ) ` m ) <_ y <-> ( ( n e. Z |-> B ) ` n ) <_ y ) )
33 29 30 32 cbvralw 
 |-  ( A. m e. Z ( ( n e. Z |-> B ) ` m ) <_ y <-> A. n e. Z ( ( n e. Z |-> B ) ` n ) <_ y )
34 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> n e. Z )
35 15 fvmpt2 
 |-  ( ( n e. Z /\ B e. RR ) -> ( ( n e. Z |-> B ) ` n ) = B )
36 34 8 35 syl2anc 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> B ) ` n ) = B )
37 36 breq1d 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( ( n e. Z |-> B ) ` n ) <_ y <-> B <_ y ) )
38 37 ralbidva 
 |-  ( ( ph /\ x e. A ) -> ( A. n e. Z ( ( n e. Z |-> B ) ` n ) <_ y <-> A. n e. Z B <_ y ) )
39 33 38 bitrid 
 |-  ( ( ph /\ x e. A ) -> ( A. m e. Z ( ( n e. Z |-> B ) ` m ) <_ y <-> A. n e. Z B <_ y ) )
40 25 39 bitrd 
 |-  ( ( ph /\ x e. A ) -> ( A. z e. ran ( n e. Z |-> B ) z <_ y <-> A. n e. Z B <_ y ) )
41 40 rexbidv 
 |-  ( ( ph /\ x e. A ) -> ( E. y e. RR A. z e. ran ( n e. Z |-> B ) z <_ y <-> E. y e. RR A. n e. Z B <_ y ) )
42 6 41 mpbird 
 |-  ( ( ph /\ x e. A ) -> E. y e. RR A. z e. ran ( n e. Z |-> B ) z <_ y )
43 10 21 42 suprcld 
 |-  ( ( ph /\ x e. A ) -> sup ( ran ( n e. Z |-> B ) , RR , < ) e. RR )
44 43 2 fmptd 
 |-  ( ph -> G : A --> RR )
45 simpr 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. A ) -> x e. A )
46 ltso 
 |-  < Or RR
47 46 supex 
 |-  sup ( ran ( n e. Z |-> B ) , RR , < ) e. _V
48 2 fvmpt2 
 |-  ( ( x e. A /\ sup ( ran ( n e. Z |-> B ) , RR , < ) e. _V ) -> ( G ` x ) = sup ( ran ( n e. Z |-> B ) , RR , < ) )
49 45 47 48 sylancl 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. A ) -> ( G ` x ) = sup ( ran ( n e. Z |-> B ) , RR , < ) )
50 49 breq2d 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. A ) -> ( t < ( G ` x ) <-> t < sup ( ran ( n e. Z |-> B ) , RR , < ) ) )
51 10 21 42 3jca 
 |-  ( ( ph /\ x e. A ) -> ( ran ( n e. Z |-> B ) C_ RR /\ ran ( n e. Z |-> B ) =/= (/) /\ E. y e. RR A. z e. ran ( n e. Z |-> B ) z <_ y ) )
52 51 adantlr 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. A ) -> ( ran ( n e. Z |-> B ) C_ RR /\ ran ( n e. Z |-> B ) =/= (/) /\ E. y e. RR A. z e. ran ( n e. Z |-> B ) z <_ y ) )
53 simplr 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. A ) -> t e. RR )
54 suprlub 
 |-  ( ( ( ran ( n e. Z |-> B ) C_ RR /\ ran ( n e. Z |-> B ) =/= (/) /\ E. y e. RR A. z e. ran ( n e. Z |-> B ) z <_ y ) /\ t e. RR ) -> ( t < sup ( ran ( n e. Z |-> B ) , RR , < ) <-> E. z e. ran ( n e. Z |-> B ) t < z ) )
55 52 53 54 syl2anc 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. A ) -> ( t < sup ( ran ( n e. Z |-> B ) , RR , < ) <-> E. z e. ran ( n e. Z |-> B ) t < z ) )
56 22 adantlr 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. A ) -> ( n e. Z |-> B ) Fn Z )
57 breq2 
 |-  ( z = ( ( n e. Z |-> B ) ` m ) -> ( t < z <-> t < ( ( n e. Z |-> B ) ` m ) ) )
58 57 rexrn 
 |-  ( ( n e. Z |-> B ) Fn Z -> ( E. z e. ran ( n e. Z |-> B ) t < z <-> E. m e. Z t < ( ( n e. Z |-> B ) ` m ) ) )
59 56 58 syl 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. A ) -> ( E. z e. ran ( n e. Z |-> B ) t < z <-> E. m e. Z t < ( ( n e. Z |-> B ) ` m ) ) )
60 nfcv 
 |-  F/_ n t
61 nfcv 
 |-  F/_ n <
62 60 61 26 nfbr 
 |-  F/ n t < ( ( n e. Z |-> B ) ` m )
63 nfv 
 |-  F/ m t < ( ( n e. Z |-> B ) ` n )
64 31 breq2d 
 |-  ( m = n -> ( t < ( ( n e. Z |-> B ) ` m ) <-> t < ( ( n e. Z |-> B ) ` n ) ) )
65 62 63 64 cbvrexw 
 |-  ( E. m e. Z t < ( ( n e. Z |-> B ) ` m ) <-> E. n e. Z t < ( ( n e. Z |-> B ) ` n ) )
66 15 fvmpt2i 
 |-  ( n e. Z -> ( ( n e. Z |-> B ) ` n ) = ( _I ` B ) )
67 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
68 67 fvmpt2i 
 |-  ( x e. A -> ( ( x e. A |-> B ) ` x ) = ( _I ` B ) )
69 68 adantl 
 |-  ( ( ph /\ x e. A ) -> ( ( x e. A |-> B ) ` x ) = ( _I ` B ) )
70 69 eqcomd 
 |-  ( ( ph /\ x e. A ) -> ( _I ` B ) = ( ( x e. A |-> B ) ` x ) )
71 66 70 sylan9eqr 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( ( n e. Z |-> B ) ` n ) = ( ( x e. A |-> B ) ` x ) )
72 71 breq2d 
 |-  ( ( ( ph /\ x e. A ) /\ n e. Z ) -> ( t < ( ( n e. Z |-> B ) ` n ) <-> t < ( ( x e. A |-> B ) ` x ) ) )
73 72 rexbidva 
 |-  ( ( ph /\ x e. A ) -> ( E. n e. Z t < ( ( n e. Z |-> B ) ` n ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` x ) ) )
74 73 adantlr 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. A ) -> ( E. n e. Z t < ( ( n e. Z |-> B ) ` n ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` x ) ) )
75 65 74 bitrid 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. A ) -> ( E. m e. Z t < ( ( n e. Z |-> B ) ` m ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` x ) ) )
76 59 75 bitrd 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. A ) -> ( E. z e. ran ( n e. Z |-> B ) t < z <-> E. n e. Z t < ( ( x e. A |-> B ) ` x ) ) )
77 50 55 76 3bitrd 
 |-  ( ( ( ph /\ t e. RR ) /\ x e. A ) -> ( t < ( G ` x ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` x ) ) )
78 77 ralrimiva 
 |-  ( ( ph /\ t e. RR ) -> A. x e. A ( t < ( G ` x ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` x ) ) )
79 nfv 
 |-  F/ z ( t < ( G ` x ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` x ) )
80 nfcv 
 |-  F/_ x t
81 nfcv 
 |-  F/_ x <
82 nfmpt1 
 |-  F/_ x ( x e. A |-> sup ( ran ( n e. Z |-> B ) , RR , < ) )
83 2 82 nfcxfr 
 |-  F/_ x G
84 nfcv 
 |-  F/_ x z
85 83 84 nffv 
 |-  F/_ x ( G ` z )
86 80 81 85 nfbr 
 |-  F/ x t < ( G ` z )
87 nfcv 
 |-  F/_ x Z
88 nffvmpt1 
 |-  F/_ x ( ( x e. A |-> B ) ` z )
89 80 81 88 nfbr 
 |-  F/ x t < ( ( x e. A |-> B ) ` z )
90 87 89 nfrexw 
 |-  F/ x E. n e. Z t < ( ( x e. A |-> B ) ` z )
91 86 90 nfbi 
 |-  F/ x ( t < ( G ` z ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` z ) )
92 fveq2 
 |-  ( x = z -> ( G ` x ) = ( G ` z ) )
93 92 breq2d 
 |-  ( x = z -> ( t < ( G ` x ) <-> t < ( G ` z ) ) )
94 fveq2 
 |-  ( x = z -> ( ( x e. A |-> B ) ` x ) = ( ( x e. A |-> B ) ` z ) )
95 94 breq2d 
 |-  ( x = z -> ( t < ( ( x e. A |-> B ) ` x ) <-> t < ( ( x e. A |-> B ) ` z ) ) )
96 95 rexbidv 
 |-  ( x = z -> ( E. n e. Z t < ( ( x e. A |-> B ) ` x ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` z ) ) )
97 93 96 bibi12d 
 |-  ( x = z -> ( ( t < ( G ` x ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` x ) ) <-> ( t < ( G ` z ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` z ) ) ) )
98 79 91 97 cbvralw 
 |-  ( A. x e. A ( t < ( G ` x ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` x ) ) <-> A. z e. A ( t < ( G ` z ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` z ) ) )
99 78 98 sylib 
 |-  ( ( ph /\ t e. RR ) -> A. z e. A ( t < ( G ` z ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` z ) ) )
100 99 r19.21bi 
 |-  ( ( ( ph /\ t e. RR ) /\ z e. A ) -> ( t < ( G ` z ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` z ) ) )
101 44 adantr 
 |-  ( ( ph /\ t e. RR ) -> G : A --> RR )
102 101 ffvelcdmda 
 |-  ( ( ( ph /\ t e. RR ) /\ z e. A ) -> ( G ` z ) e. RR )
103 rexr 
 |-  ( t e. RR -> t e. RR* )
104 103 ad2antlr 
 |-  ( ( ( ph /\ t e. RR ) /\ z e. A ) -> t e. RR* )
105 elioopnf 
 |-  ( t e. RR* -> ( ( G ` z ) e. ( t (,) +oo ) <-> ( ( G ` z ) e. RR /\ t < ( G ` z ) ) ) )
106 104 105 syl 
 |-  ( ( ( ph /\ t e. RR ) /\ z e. A ) -> ( ( G ` z ) e. ( t (,) +oo ) <-> ( ( G ` z ) e. RR /\ t < ( G ` z ) ) ) )
107 102 106 mpbirand 
 |-  ( ( ( ph /\ t e. RR ) /\ z e. A ) -> ( ( G ` z ) e. ( t (,) +oo ) <-> t < ( G ` z ) ) )
108 104 adantr 
 |-  ( ( ( ( ph /\ t e. RR ) /\ z e. A ) /\ n e. Z ) -> t e. RR* )
109 elioopnf 
 |-  ( t e. RR* -> ( ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) <-> ( ( ( x e. A |-> B ) ` z ) e. RR /\ t < ( ( x e. A |-> B ) ` z ) ) ) )
110 108 109 syl 
 |-  ( ( ( ( ph /\ t e. RR ) /\ z e. A ) /\ n e. Z ) -> ( ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) <-> ( ( ( x e. A |-> B ) ` z ) e. RR /\ t < ( ( x e. A |-> B ) ` z ) ) ) )
111 7 fmpttd 
 |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) : A --> RR )
112 111 ffvelcdmda 
 |-  ( ( ( ph /\ n e. Z ) /\ z e. A ) -> ( ( x e. A |-> B ) ` z ) e. RR )
113 112 biantrurd 
 |-  ( ( ( ph /\ n e. Z ) /\ z e. A ) -> ( t < ( ( x e. A |-> B ) ` z ) <-> ( ( ( x e. A |-> B ) ` z ) e. RR /\ t < ( ( x e. A |-> B ) ` z ) ) ) )
114 113 an32s 
 |-  ( ( ( ph /\ z e. A ) /\ n e. Z ) -> ( t < ( ( x e. A |-> B ) ` z ) <-> ( ( ( x e. A |-> B ) ` z ) e. RR /\ t < ( ( x e. A |-> B ) ` z ) ) ) )
115 114 adantllr 
 |-  ( ( ( ( ph /\ t e. RR ) /\ z e. A ) /\ n e. Z ) -> ( t < ( ( x e. A |-> B ) ` z ) <-> ( ( ( x e. A |-> B ) ` z ) e. RR /\ t < ( ( x e. A |-> B ) ` z ) ) ) )
116 110 115 bitr4d 
 |-  ( ( ( ( ph /\ t e. RR ) /\ z e. A ) /\ n e. Z ) -> ( ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) <-> t < ( ( x e. A |-> B ) ` z ) ) )
117 116 rexbidva 
 |-  ( ( ( ph /\ t e. RR ) /\ z e. A ) -> ( E. n e. Z ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) <-> E. n e. Z t < ( ( x e. A |-> B ) ` z ) ) )
118 100 107 117 3bitr4d 
 |-  ( ( ( ph /\ t e. RR ) /\ z e. A ) -> ( ( G ` z ) e. ( t (,) +oo ) <-> E. n e. Z ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) ) )
119 118 pm5.32da 
 |-  ( ( ph /\ t e. RR ) -> ( ( z e. A /\ ( G ` z ) e. ( t (,) +oo ) ) <-> ( z e. A /\ E. n e. Z ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) ) ) )
120 44 ffnd 
 |-  ( ph -> G Fn A )
121 120 adantr 
 |-  ( ( ph /\ t e. RR ) -> G Fn A )
122 elpreima 
 |-  ( G Fn A -> ( z e. ( `' G " ( t (,) +oo ) ) <-> ( z e. A /\ ( G ` z ) e. ( t (,) +oo ) ) ) )
123 121 122 syl 
 |-  ( ( ph /\ t e. RR ) -> ( z e. ( `' G " ( t (,) +oo ) ) <-> ( z e. A /\ ( G ` z ) e. ( t (,) +oo ) ) ) )
124 eliun 
 |-  ( z e. U_ n e. Z ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) <-> E. n e. Z z e. ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) )
125 111 ffnd 
 |-  ( ( ph /\ n e. Z ) -> ( x e. A |-> B ) Fn A )
126 elpreima 
 |-  ( ( x e. A |-> B ) Fn A -> ( z e. ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) <-> ( z e. A /\ ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) ) ) )
127 125 126 syl 
 |-  ( ( ph /\ n e. Z ) -> ( z e. ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) <-> ( z e. A /\ ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) ) ) )
128 127 rexbidva 
 |-  ( ph -> ( E. n e. Z z e. ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) <-> E. n e. Z ( z e. A /\ ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) ) ) )
129 128 adantr 
 |-  ( ( ph /\ t e. RR ) -> ( E. n e. Z z e. ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) <-> E. n e. Z ( z e. A /\ ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) ) ) )
130 r19.42v 
 |-  ( E. n e. Z ( z e. A /\ ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) ) <-> ( z e. A /\ E. n e. Z ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) ) )
131 129 130 bitrdi 
 |-  ( ( ph /\ t e. RR ) -> ( E. n e. Z z e. ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) <-> ( z e. A /\ E. n e. Z ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) ) ) )
132 124 131 bitrid 
 |-  ( ( ph /\ t e. RR ) -> ( z e. U_ n e. Z ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) <-> ( z e. A /\ E. n e. Z ( ( x e. A |-> B ) ` z ) e. ( t (,) +oo ) ) ) )
133 119 123 132 3bitr4d 
 |-  ( ( ph /\ t e. RR ) -> ( z e. ( `' G " ( t (,) +oo ) ) <-> z e. U_ n e. Z ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) ) )
134 133 eqrdv 
 |-  ( ( ph /\ t e. RR ) -> ( `' G " ( t (,) +oo ) ) = U_ n e. Z ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) )
135 zex 
 |-  ZZ e. _V
136 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
137 ssdomg 
 |-  ( ZZ e. _V -> ( ( ZZ>= ` M ) C_ ZZ -> ( ZZ>= ` M ) ~<_ ZZ ) )
138 135 136 137 mp2 
 |-  ( ZZ>= ` M ) ~<_ ZZ
139 1 138 eqbrtri 
 |-  Z ~<_ ZZ
140 znnen 
 |-  ZZ ~~ NN
141 domentr 
 |-  ( ( Z ~<_ ZZ /\ ZZ ~~ NN ) -> Z ~<_ NN )
142 139 140 141 mp2an 
 |-  Z ~<_ NN
143 mbfima 
 |-  ( ( ( x e. A |-> B ) e. MblFn /\ ( x e. A |-> B ) : A --> RR ) -> ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) e. dom vol )
144 4 111 143 syl2anc 
 |-  ( ( ph /\ n e. Z ) -> ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) e. dom vol )
145 144 ralrimiva 
 |-  ( ph -> A. n e. Z ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) e. dom vol )
146 145 adantr 
 |-  ( ( ph /\ t e. RR ) -> A. n e. Z ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) e. dom vol )
147 iunmbl2 
 |-  ( ( Z ~<_ NN /\ A. n e. Z ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) e. dom vol ) -> U_ n e. Z ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) e. dom vol )
148 142 146 147 sylancr 
 |-  ( ( ph /\ t e. RR ) -> U_ n e. Z ( `' ( x e. A |-> B ) " ( t (,) +oo ) ) e. dom vol )
149 134 148 eqeltrd 
 |-  ( ( ph /\ t e. RR ) -> ( `' G " ( t (,) +oo ) ) e. dom vol )
150 44 149 ismbf3d 
 |-  ( ph -> G e. MblFn )