Metamath Proof Explorer

Theorem meaiuninc3v

Description: Measures are continuous from below: if E is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is the general case of Proposition 112C (e) of Fremlin1 p. 16 . This theorem generalizes meaiuninc and meaiuninc2 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022)

Ref Expression
Hypotheses meaiuninc3v.m 
|- ( ph -> M e. Meas )
meaiuninc3v.n 
|- ( ph -> N e. ZZ )
meaiuninc3v.z 
|- Z = ( ZZ>= ` N )
meaiuninc3v.e 
|- ( ph -> E : Z --> dom M )
meaiuninc3v.i 
|- ( ( ph /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) )
meaiuninc3v.s 
|- S = ( n e. Z |-> ( M ` ( E ` n ) ) )
Assertion meaiuninc3v 
|- ( ph -> S ~~>* ( M ` U_ n e. Z ( E ` n ) ) )

Proof

Step Hyp Ref Expression
1 meaiuninc3v.m 
 |-  ( ph -> M e. Meas )
2 meaiuninc3v.n 
 |-  ( ph -> N e. ZZ )
3 meaiuninc3v.z 
 |-  Z = ( ZZ>= ` N )
4 meaiuninc3v.e 
 |-  ( ph -> E : Z --> dom M )
5 meaiuninc3v.i 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) )
6 meaiuninc3v.s 
 |-  S = ( n e. Z |-> ( M ` ( E ` n ) ) )
7 2 adantr 
 |-  ( ( ph /\ E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> N e. ZZ )
8 1 adantr 
 |-  ( ( ph /\ n e. Z ) -> M e. Meas )
9 eqid 
 |-  dom M = dom M
10 4 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( E ` n ) e. dom M )
11 8 9 10 meaxrcl 
 |-  ( ( ph /\ n e. Z ) -> ( M ` ( E ` n ) ) e. RR* )
12 11 6 fmptd 
 |-  ( ph -> S : Z --> RR* )
13 12 adantr 
 |-  ( ( ph /\ E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> S : Z --> RR* )
14 nfv 
 |-  F/ n ph
15 nfcv 
 |-  F/_ n RR
16 nfra1 
 |-  F/ n A. n e. Z ( M ` ( E ` n ) ) <_ x
17 15 16 nfrex 
 |-  F/ n E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x
18 14 17 nfan 
 |-  F/ n ( ph /\ E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x )
19 nfcv 
 |-  F/_ n E
20 1 adantr 
 |-  ( ( ph /\ E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> M e. Meas )
21 4 adantr 
 |-  ( ( ph /\ E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> E : Z --> dom M )
22 5 adantlr 
 |-  ( ( ( ph /\ E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) )
23 simpr 
 |-  ( ( ph /\ E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x )
24 18 19 20 7 3 21 22 23 6 meaiunincf 
 |-  ( ( ph /\ E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> S ~~> ( M ` U_ n e. Z ( E ` n ) ) )
25 7 3 13 24 climxlim2 
 |-  ( ( ph /\ E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> S ~~>* ( M ` U_ n e. Z ( E ` n ) ) )
26 simpr 
 |-  ( ( ph /\ -. E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> -. E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x )
27 2fveq3 
 |-  ( j = n -> ( M ` ( E ` j ) ) = ( M ` ( E ` n ) ) )
28 27 breq2d 
 |-  ( j = n -> ( x < ( M ` ( E ` j ) ) <-> x < ( M ` ( E ` n ) ) ) )
29 28 cbvrexvw 
 |-  ( E. j e. Z x < ( M ` ( E ` j ) ) <-> E. n e. Z x < ( M ` ( E ` n ) ) )
30 29 a1i 
 |-  ( ( ph /\ x e. RR ) -> ( E. j e. Z x < ( M ` ( E ` j ) ) <-> E. n e. Z x < ( M ` ( E ` n ) ) ) )
31 rexr 
 |-  ( x e. RR -> x e. RR* )
32 31 ad2antlr 
 |-  ( ( ( ph /\ x e. RR ) /\ n e. Z ) -> x e. RR* )
33 11 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ n e. Z ) -> ( M ` ( E ` n ) ) e. RR* )
34 32 33 xrltnled 
 |-  ( ( ( ph /\ x e. RR ) /\ n e. Z ) -> ( x < ( M ` ( E ` n ) ) <-> -. ( M ` ( E ` n ) ) <_ x ) )
35 34 rexbidva 
 |-  ( ( ph /\ x e. RR ) -> ( E. n e. Z x < ( M ` ( E ` n ) ) <-> E. n e. Z -. ( M ` ( E ` n ) ) <_ x ) )
36 30 35 bitrd 
 |-  ( ( ph /\ x e. RR ) -> ( E. j e. Z x < ( M ` ( E ` j ) ) <-> E. n e. Z -. ( M ` ( E ` n ) ) <_ x ) )
37 36 ralbidva 
 |-  ( ph -> ( A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) <-> A. x e. RR E. n e. Z -. ( M ` ( E ` n ) ) <_ x ) )
38 rexnal 
 |-  ( E. n e. Z -. ( M ` ( E ` n ) ) <_ x <-> -. A. n e. Z ( M ` ( E ` n ) ) <_ x )
39 38 ralbii 
 |-  ( A. x e. RR E. n e. Z -. ( M ` ( E ` n ) ) <_ x <-> A. x e. RR -. A. n e. Z ( M ` ( E ` n ) ) <_ x )
40 ralnex 
 |-  ( A. x e. RR -. A. n e. Z ( M ` ( E ` n ) ) <_ x <-> -. E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x )
41 39 40 bitri 
 |-  ( A. x e. RR E. n e. Z -. ( M ` ( E ` n ) ) <_ x <-> -. E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x )
42 41 a1i 
 |-  ( ph -> ( A. x e. RR E. n e. Z -. ( M ` ( E ` n ) ) <_ x <-> -. E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) )
43 37 42 bitrd 
 |-  ( ph -> ( A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) <-> -. E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) )
44 43 adantr 
 |-  ( ( ph /\ -. E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> ( A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) <-> -. E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) )
45 26 44 mpbird 
 |-  ( ( ph /\ -. E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) )
46 simpr 
 |-  ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) -> A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) )
47 45 46 syldan 
 |-  ( ( ph /\ -. E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) )
48 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) /\ n e. ( ZZ>= ` j ) ) -> x e. RR )
49 48 31 syl 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) /\ n e. ( ZZ>= ` j ) ) -> x e. RR* )
50 simp-4l 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) /\ n e. ( ZZ>= ` j ) ) -> ph )
51 3 uztrn2 
 |-  ( ( j e. Z /\ n e. ( ZZ>= ` j ) ) -> n e. Z )
52 51 ad4ant24 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) /\ n e. ( ZZ>= ` j ) ) -> n e. Z )
53 12 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( S ` n ) e. RR* )
54 50 52 53 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) /\ n e. ( ZZ>= ` j ) ) -> ( S ` n ) e. RR* )
55 eleq1w 
 |-  ( n = j -> ( n e. Z <-> j e. Z ) )
56 55 anbi2d 
 |-  ( n = j -> ( ( ph /\ n e. Z ) <-> ( ph /\ j e. Z ) ) )
57 2fveq3 
 |-  ( n = j -> ( M ` ( E ` n ) ) = ( M ` ( E ` j ) ) )
58 57 eleq1d 
 |-  ( n = j -> ( ( M ` ( E ` n ) ) e. RR* <-> ( M ` ( E ` j ) ) e. RR* ) )
59 56 58 imbi12d 
 |-  ( n = j -> ( ( ( ph /\ n e. Z ) -> ( M ` ( E ` n ) ) e. RR* ) <-> ( ( ph /\ j e. Z ) -> ( M ` ( E ` j ) ) e. RR* ) ) )
60 59 11 chvarvv 
 |-  ( ( ph /\ j e. Z ) -> ( M ` ( E ` j ) ) e. RR* )
61 60 ad5ant13 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) /\ n e. ( ZZ>= ` j ) ) -> ( M ` ( E ` j ) ) e. RR* )
62 simplr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) /\ n e. ( ZZ>= ` j ) ) -> x < ( M ` ( E ` j ) ) )
63 1 3ad2ant1 
 |-  ( ( ph /\ j e. Z /\ n e. ( ZZ>= ` j ) ) -> M e. Meas )
64 4 ffvelrnda 
 |-  ( ( ph /\ j e. Z ) -> ( E ` j ) e. dom M )
65 64 3adant3 
 |-  ( ( ph /\ j e. Z /\ n e. ( ZZ>= ` j ) ) -> ( E ` j ) e. dom M )
66 simp1 
 |-  ( ( ph /\ j e. Z /\ n e. ( ZZ>= ` j ) ) -> ph )
67 51 3adant1 
 |-  ( ( ph /\ j e. Z /\ n e. ( ZZ>= ` j ) ) -> n e. Z )
68 66 67 10 syl2anc 
 |-  ( ( ph /\ j e. Z /\ n e. ( ZZ>= ` j ) ) -> ( E ` n ) e. dom M )
69 simp3 
 |-  ( ( ph /\ j e. Z /\ n e. ( ZZ>= ` j ) ) -> n e. ( ZZ>= ` j ) )
70 simpll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( j ..^ n ) ) -> ph )
71 3 uzssd3 
 |-  ( j e. Z -> ( ZZ>= ` j ) C_ Z )
72 71 adantr 
 |-  ( ( j e. Z /\ k e. ( j ..^ n ) ) -> ( ZZ>= ` j ) C_ Z )
73 elfzouz 
 |-  ( k e. ( j ..^ n ) -> k e. ( ZZ>= ` j ) )
74 73 adantl 
 |-  ( ( j e. Z /\ k e. ( j ..^ n ) ) -> k e. ( ZZ>= ` j ) )
75 72 74 sseldd 
 |-  ( ( j e. Z /\ k e. ( j ..^ n ) ) -> k e. Z )
76 75 adantll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( j ..^ n ) ) -> k e. Z )
77 eleq1w 
 |-  ( n = k -> ( n e. Z <-> k e. Z ) )
78 77 anbi2d 
 |-  ( n = k -> ( ( ph /\ n e. Z ) <-> ( ph /\ k e. Z ) ) )
79 fveq2 
 |-  ( n = k -> ( E ` n ) = ( E ` k ) )
80 fvoveq1 
 |-  ( n = k -> ( E ` ( n + 1 ) ) = ( E ` ( k + 1 ) ) )
81 79 80 sseq12d 
 |-  ( n = k -> ( ( E ` n ) C_ ( E ` ( n + 1 ) ) <-> ( E ` k ) C_ ( E ` ( k + 1 ) ) ) )
82 78 81 imbi12d 
 |-  ( n = k -> ( ( ( ph /\ n e. Z ) -> ( E ` n ) C_ ( E ` ( n + 1 ) ) ) <-> ( ( ph /\ k e. Z ) -> ( E ` k ) C_ ( E ` ( k + 1 ) ) ) ) )
83 82 5 chvarvv 
 |-  ( ( ph /\ k e. Z ) -> ( E ` k ) C_ ( E ` ( k + 1 ) ) )
84 70 76 83 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( j ..^ n ) ) -> ( E ` k ) C_ ( E ` ( k + 1 ) ) )
85 84 3adantl3 
 |-  ( ( ( ph /\ j e. Z /\ n e. ( ZZ>= ` j ) ) /\ k e. ( j ..^ n ) ) -> ( E ` k ) C_ ( E ` ( k + 1 ) ) )
86 69 85 ssinc 
 |-  ( ( ph /\ j e. Z /\ n e. ( ZZ>= ` j ) ) -> ( E ` j ) C_ ( E ` n ) )
87 63 9 65 68 86 meassle 
 |-  ( ( ph /\ j e. Z /\ n e. ( ZZ>= ` j ) ) -> ( M ` ( E ` j ) ) <_ ( M ` ( E ` n ) ) )
88 fvexd 
 |-  ( ( j e. Z /\ n e. ( ZZ>= ` j ) ) -> ( M ` ( E ` n ) ) e. _V )
89 6 fvmpt2 
 |-  ( ( n e. Z /\ ( M ` ( E ` n ) ) e. _V ) -> ( S ` n ) = ( M ` ( E ` n ) ) )
90 51 88 89 syl2anc 
 |-  ( ( j e. Z /\ n e. ( ZZ>= ` j ) ) -> ( S ` n ) = ( M ` ( E ` n ) ) )
91 90 3adant1 
 |-  ( ( ph /\ j e. Z /\ n e. ( ZZ>= ` j ) ) -> ( S ` n ) = ( M ` ( E ` n ) ) )
92 87 91 breqtrrd 
 |-  ( ( ph /\ j e. Z /\ n e. ( ZZ>= ` j ) ) -> ( M ` ( E ` j ) ) <_ ( S ` n ) )
93 92 ad5ant135 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) /\ n e. ( ZZ>= ` j ) ) -> ( M ` ( E ` j ) ) <_ ( S ` n ) )
94 49 61 54 62 93 xrltletrd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) /\ n e. ( ZZ>= ` j ) ) -> x < ( S ` n ) )
95 49 54 94 xrltled 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) /\ n e. ( ZZ>= ` j ) ) -> x <_ ( S ` n ) )
96 95 ralrimiva 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) -> A. n e. ( ZZ>= ` j ) x <_ ( S ` n ) )
97 96 ex 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. Z ) -> ( x < ( M ` ( E ` j ) ) -> A. n e. ( ZZ>= ` j ) x <_ ( S ` n ) ) )
98 97 reximdva 
 |-  ( ( ph /\ x e. RR ) -> ( E. j e. Z x < ( M ` ( E ` j ) ) -> E. j e. Z A. n e. ( ZZ>= ` j ) x <_ ( S ` n ) ) )
99 98 ralimdva 
 |-  ( ph -> ( A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) -> A. x e. RR E. j e. Z A. n e. ( ZZ>= ` j ) x <_ ( S ` n ) ) )
100 99 imp 
 |-  ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) -> A. x e. RR E. j e. Z A. n e. ( ZZ>= ` j ) x <_ ( S ` n ) )
101 nfmpt1 
 |-  F/_ n ( n e. Z |-> ( M ` ( E ` n ) ) )
102 6 101 nfcxfr 
 |-  F/_ n S
103 102 2 3 12 xlimpnf 
 |-  ( ph -> ( S ~~>* +oo <-> A. x e. RR E. j e. Z A. n e. ( ZZ>= ` j ) x <_ ( S ` n ) ) )
104 103 adantr 
 |-  ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) -> ( S ~~>* +oo <-> A. x e. RR E. j e. Z A. n e. ( ZZ>= ` j ) x <_ ( S ` n ) ) )
105 100 104 mpbird 
 |-  ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) -> S ~~>* +oo )
106 nfv 
 |-  F/ x ph
107 nfra1 
 |-  F/ x A. x e. RR E. j e. Z x < ( M ` ( E ` j ) )
108 106 107 nfan 
 |-  F/ x ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) )
109 rspa 
 |-  ( ( A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) /\ x e. RR ) -> E. j e. Z x < ( M ` ( E ` j ) ) )
110 109 adantll 
 |-  ( ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) /\ x e. RR ) -> E. j e. Z x < ( M ` ( E ` j ) ) )
111 nfv 
 |-  F/ j ph
112 nfcv 
 |-  F/_ j RR
113 nfre1 
 |-  F/ j E. j e. Z x < ( M ` ( E ` j ) )
114 112 113 nfralw 
 |-  F/ j A. x e. RR E. j e. Z x < ( M ` ( E ` j ) )
115 111 114 nfan 
 |-  F/ j ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) )
116 nfv 
 |-  F/ j x e. RR
117 115 116 nfan 
 |-  F/ j ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) /\ x e. RR )
118 nfv 
 |-  F/ j x <_ ( M ` U_ n e. Z ( E ` n ) )
119 31 ad3antlr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) -> x e. RR* )
120 1 9 dmmeasal 
 |-  ( ph -> dom M e. SAlg )
121 3 uzct 
 |-  Z ~<_ _om
122 121 a1i 
 |-  ( ph -> Z ~<_ _om )
123 120 122 10 saliuncl 
 |-  ( ph -> U_ n e. Z ( E ` n ) e. dom M )
124 1 9 123 meaxrcl 
 |-  ( ph -> ( M ` U_ n e. Z ( E ` n ) ) e. RR* )
125 124 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) -> ( M ` U_ n e. Z ( E ` n ) ) e. RR* )
126 60 ad4ant13 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) -> ( M ` ( E ` j ) ) e. RR* )
127 simpr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) -> x < ( M ` ( E ` j ) ) )
128 1 adantr 
 |-  ( ( ph /\ j e. Z ) -> M e. Meas )
129 123 adantr 
 |-  ( ( ph /\ j e. Z ) -> U_ n e. Z ( E ` n ) e. dom M )
130 fveq2 
 |-  ( n = j -> ( E ` n ) = ( E ` j ) )
131 130 ssiun2s 
 |-  ( j e. Z -> ( E ` j ) C_ U_ n e. Z ( E ` n ) )
132 131 adantl 
 |-  ( ( ph /\ j e. Z ) -> ( E ` j ) C_ U_ n e. Z ( E ` n ) )
133 128 9 64 129 132 meassle 
 |-  ( ( ph /\ j e. Z ) -> ( M ` ( E ` j ) ) <_ ( M ` U_ n e. Z ( E ` n ) ) )
134 133 ad4ant13 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) -> ( M ` ( E ` j ) ) <_ ( M ` U_ n e. Z ( E ` n ) ) )
135 119 126 125 127 134 xrltletrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) -> x < ( M ` U_ n e. Z ( E ` n ) ) )
136 119 125 135 xrltled 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ x < ( M ` ( E ` j ) ) ) -> x <_ ( M ` U_ n e. Z ( E ` n ) ) )
137 136 exp31 
 |-  ( ( ph /\ x e. RR ) -> ( j e. Z -> ( x < ( M ` ( E ` j ) ) -> x <_ ( M ` U_ n e. Z ( E ` n ) ) ) ) )
138 137 adantlr 
 |-  ( ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) /\ x e. RR ) -> ( j e. Z -> ( x < ( M ` ( E ` j ) ) -> x <_ ( M ` U_ n e. Z ( E ` n ) ) ) ) )
139 117 118 138 rexlimd 
 |-  ( ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) /\ x e. RR ) -> ( E. j e. Z x < ( M ` ( E ` j ) ) -> x <_ ( M ` U_ n e. Z ( E ` n ) ) ) )
140 110 139 mpd 
 |-  ( ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) /\ x e. RR ) -> x <_ ( M ` U_ n e. Z ( E ` n ) ) )
141 108 140 ralrimia 
 |-  ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) -> A. x e. RR x <_ ( M ` U_ n e. Z ( E ` n ) ) )
142 xrpnf 
 |-  ( ( M ` U_ n e. Z ( E ` n ) ) e. RR* -> ( ( M ` U_ n e. Z ( E ` n ) ) = +oo <-> A. x e. RR x <_ ( M ` U_ n e. Z ( E ` n ) ) ) )
143 124 142 syl 
 |-  ( ph -> ( ( M ` U_ n e. Z ( E ` n ) ) = +oo <-> A. x e. RR x <_ ( M ` U_ n e. Z ( E ` n ) ) ) )
144 143 adantr 
 |-  ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) -> ( ( M ` U_ n e. Z ( E ` n ) ) = +oo <-> A. x e. RR x <_ ( M ` U_ n e. Z ( E ` n ) ) ) )
145 141 144 mpbird 
 |-  ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) -> ( M ` U_ n e. Z ( E ` n ) ) = +oo )
146 105 145 breqtrrd 
 |-  ( ( ph /\ A. x e. RR E. j e. Z x < ( M ` ( E ` j ) ) ) -> S ~~>* ( M ` U_ n e. Z ( E ` n ) ) )
147 47 146 syldan 
 |-  ( ( ph /\ -. E. x e. RR A. n e. Z ( M ` ( E ` n ) ) <_ x ) -> S ~~>* ( M ` U_ n e. Z ( E ` n ) ) )
148 25 147 pm2.61dan 
 |-  ( ph -> S ~~>* ( M ` U_ n e. Z ( E ` n ) ) )