Metamath Proof Explorer

Theorem smfsuplem1

Description: The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smfsuplem1.m 
|- ( ph -> M e. ZZ )
smfsuplem1.z 
|- Z = ( ZZ>= ` M )
smfsuplem1.s 
|- ( ph -> S e. SAlg )
smfsuplem1.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smfsuplem1.d 
|- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
smfsuplem1.g 
|- G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
smfsuplem1.a 
|- ( ph -> A e. RR )
smfsuplem1.h 
|- ( ph -> H : Z --> S )
smfsuplem1.i 
|- ( ( ph /\ n e. Z ) -> ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( H ` n ) i^i dom ( F ` n ) ) )
Assertion smfsuplem1 
|- ( ph -> ( `' G " ( -oo (,] A ) ) e. ( S |`t D ) )

Proof

Step Hyp Ref Expression
1 smfsuplem1.m 
 |-  ( ph -> M e. ZZ )
2 smfsuplem1.z 
 |-  Z = ( ZZ>= ` M )
3 smfsuplem1.s 
 |-  ( ph -> S e. SAlg )
4 smfsuplem1.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
5 smfsuplem1.d 
 |-  D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
6 smfsuplem1.g 
 |-  G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
7 smfsuplem1.a 
 |-  ( ph -> A e. RR )
8 smfsuplem1.h 
 |-  ( ph -> H : Z --> S )
9 smfsuplem1.i 
 |-  ( ( ph /\ n e. Z ) -> ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( H ` n ) i^i dom ( F ` n ) ) )
10 3 adantr 
 |-  ( ( ph /\ n e. Z ) -> S e. SAlg )
11 4 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. ( SMblFn ` S ) )
12 eqid 
 |-  dom ( F ` n ) = dom ( F ` n )
13 10 11 12 smff 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR )
14 13 ffnd 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) Fn dom ( F ` n ) )
15 14 adantr 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( F ` n ) Fn dom ( F ` n ) )
16 ssrab2 
 |-  { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } C_ |^|_ n e. Z dom ( F ` n )
17 5 16 eqsstri 
 |-  D C_ |^|_ n e. Z dom ( F ` n )
18 iinss2 
 |-  ( n e. Z -> |^|_ n e. Z dom ( F ` n ) C_ dom ( F ` n ) )
19 17 18 sstrid 
 |-  ( n e. Z -> D C_ dom ( F ` n ) )
20 19 ad2antlr 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> D C_ dom ( F ` n ) )
21 cnvimass 
 |-  ( `' G " ( -oo (,] A ) ) C_ dom G
22 21 sseli 
 |-  ( x e. ( `' G " ( -oo (,] A ) ) -> x e. dom G )
23 22 adantl 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> x e. dom G )
24 nfv 
 |-  F/ n ( ph /\ x e. D )
25 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
26 1 25 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
27 26 2 eleqtrrdi 
 |-  ( ph -> M e. Z )
28 27 ne0d 
 |-  ( ph -> Z =/= (/) )
29 28 adantr 
 |-  ( ( ph /\ x e. D ) -> Z =/= (/) )
30 13 adantlr 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR )
31 18 adantl 
 |-  ( ( x e. D /\ n e. Z ) -> |^|_ n e. Z dom ( F ` n ) C_ dom ( F ` n ) )
32 17 sseli 
 |-  ( x e. D -> x e. |^|_ n e. Z dom ( F ` n ) )
33 32 adantr 
 |-  ( ( x e. D /\ n e. Z ) -> x e. |^|_ n e. Z dom ( F ` n ) )
34 31 33 sseldd 
 |-  ( ( x e. D /\ n e. Z ) -> x e. dom ( F ` n ) )
35 34 adantll 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> x e. dom ( F ` n ) )
36 30 35 ffvelcdmd 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR )
37 5 reqabi 
 |-  ( x e. D <-> ( x e. |^|_ n e. Z dom ( F ` n ) /\ E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y ) )
38 37 simprbi 
 |-  ( x e. D -> E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y )
39 38 adantl 
 |-  ( ( ph /\ x e. D ) -> E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y )
40 24 29 36 39 suprclrnmpt 
 |-  ( ( ph /\ x e. D ) -> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) e. RR )
41 40 6 fmptd 
 |-  ( ph -> G : D --> RR )
42 41 fdmd 
 |-  ( ph -> dom G = D )
43 42 ad2antrr 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> dom G = D )
44 23 43 eleqtrd 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> x e. D )
45 20 44 sseldd 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> x e. dom ( F ` n ) )
46 mnfxr 
 |-  -oo e. RR*
47 46 a1i 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> -oo e. RR* )
48 7 rexrd 
 |-  ( ph -> A e. RR* )
49 48 ad2antrr 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> A e. RR* )
50 36 an32s 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. D ) -> ( ( F ` n ) ` x ) e. RR )
51 44 50 syldan 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( ( F ` n ) ` x ) e. RR )
52 51 rexrd 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( ( F ` n ) ` x ) e. RR* )
53 51 mnfltd 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> -oo < ( ( F ` n ) ` x ) )
54 22 adantl 
 |-  ( ( ph /\ x e. ( `' G " ( -oo (,] A ) ) ) -> x e. dom G )
55 41 ffdmd 
 |-  ( ph -> G : dom G --> RR )
56 55 ffvelcdmda 
 |-  ( ( ph /\ x e. dom G ) -> ( G ` x ) e. RR )
57 54 56 syldan 
 |-  ( ( ph /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( G ` x ) e. RR )
58 57 adantlr 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( G ` x ) e. RR )
59 7 ad2antrr 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> A e. RR )
60 an32 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. D ) <-> ( ( ph /\ x e. D ) /\ n e. Z ) )
61 60 biimpi 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. D ) -> ( ( ph /\ x e. D ) /\ n e. Z ) )
62 24 36 39 suprubrnmpt 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ( ( F ` n ) ` x ) <_ sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
63 61 62 syl 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. D ) -> ( ( F ` n ) ` x ) <_ sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
64 6 a1i 
 |-  ( ph -> G = ( x e. D |-> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) )
65 64 40 fvmpt2d 
 |-  ( ( ph /\ x e. D ) -> ( G ` x ) = sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
66 65 adantlr 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. D ) -> ( G ` x ) = sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
67 63 66 breqtrrd 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. D ) -> ( ( F ` n ) ` x ) <_ ( G ` x ) )
68 44 67 syldan 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( ( F ` n ) ` x ) <_ ( G ` x ) )
69 46 a1i 
 |-  ( ( ph /\ x e. ( `' G " ( -oo (,] A ) ) ) -> -oo e. RR* )
70 48 adantr 
 |-  ( ( ph /\ x e. ( `' G " ( -oo (,] A ) ) ) -> A e. RR* )
71 simpr 
 |-  ( ( ph /\ x e. ( `' G " ( -oo (,] A ) ) ) -> x e. ( `' G " ( -oo (,] A ) ) )
72 41 ffnd 
 |-  ( ph -> G Fn D )
73 elpreima 
 |-  ( G Fn D -> ( x e. ( `' G " ( -oo (,] A ) ) <-> ( x e. D /\ ( G ` x ) e. ( -oo (,] A ) ) ) )
74 72 73 syl 
 |-  ( ph -> ( x e. ( `' G " ( -oo (,] A ) ) <-> ( x e. D /\ ( G ` x ) e. ( -oo (,] A ) ) ) )
75 74 adantr 
 |-  ( ( ph /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( x e. ( `' G " ( -oo (,] A ) ) <-> ( x e. D /\ ( G ` x ) e. ( -oo (,] A ) ) ) )
76 71 75 mpbid 
 |-  ( ( ph /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( x e. D /\ ( G ` x ) e. ( -oo (,] A ) ) )
77 76 simprd 
 |-  ( ( ph /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( G ` x ) e. ( -oo (,] A ) )
78 69 70 77 iocleubd 
 |-  ( ( ph /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( G ` x ) <_ A )
79 78 adantlr 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( G ` x ) <_ A )
80 51 58 59 68 79 letrd 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( ( F ` n ) ` x ) <_ A )
81 47 49 52 53 80 eliocd 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> ( ( F ` n ) ` x ) e. ( -oo (,] A ) )
82 15 45 81 elpreimad 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. ( `' G " ( -oo (,] A ) ) ) -> x e. ( `' ( F ` n ) " ( -oo (,] A ) ) )
83 82 ssd 
 |-  ( ( ph /\ n e. Z ) -> ( `' G " ( -oo (,] A ) ) C_ ( `' ( F ` n ) " ( -oo (,] A ) ) )
84 inss1 
 |-  ( ( H ` n ) i^i dom ( F ` n ) ) C_ ( H ` n )
85 9 84 eqsstrdi 
 |-  ( ( ph /\ n e. Z ) -> ( `' ( F ` n ) " ( -oo (,] A ) ) C_ ( H ` n ) )
86 83 85 sstrd 
 |-  ( ( ph /\ n e. Z ) -> ( `' G " ( -oo (,] A ) ) C_ ( H ` n ) )
87 86 ralrimiva 
 |-  ( ph -> A. n e. Z ( `' G " ( -oo (,] A ) ) C_ ( H ` n ) )
88 ssiin 
 |-  ( ( `' G " ( -oo (,] A ) ) C_ |^|_ n e. Z ( H ` n ) <-> A. n e. Z ( `' G " ( -oo (,] A ) ) C_ ( H ` n ) )
89 87 88 sylibr 
 |-  ( ph -> ( `' G " ( -oo (,] A ) ) C_ |^|_ n e. Z ( H ` n ) )
90 21 41 fssdm 
 |-  ( ph -> ( `' G " ( -oo (,] A ) ) C_ D )
91 89 90 ssind 
 |-  ( ph -> ( `' G " ( -oo (,] A ) ) C_ ( |^|_ n e. Z ( H ` n ) i^i D ) )
92 iniin1 
 |-  ( Z =/= (/) -> ( |^|_ n e. Z ( H ` n ) i^i D ) = |^|_ n e. Z ( ( H ` n ) i^i D ) )
93 28 92 syl 
 |-  ( ph -> ( |^|_ n e. Z ( H ` n ) i^i D ) = |^|_ n e. Z ( ( H ` n ) i^i D ) )
94 72 adantr 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> G Fn D )
95 simpr 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> x e. |^|_ n e. Z ( ( H ` n ) i^i D ) )
96 27 adantr 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> M e. Z )
97 fveq2 
 |-  ( n = M -> ( H ` n ) = ( H ` M ) )
98 97 ineq1d 
 |-  ( n = M -> ( ( H ` n ) i^i D ) = ( ( H ` M ) i^i D ) )
99 98 eleq2d 
 |-  ( n = M -> ( x e. ( ( H ` n ) i^i D ) <-> x e. ( ( H ` M ) i^i D ) ) )
100 95 96 99 eliind 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> x e. ( ( H ` M ) i^i D ) )
101 elinel2 
 |-  ( x e. ( ( H ` M ) i^i D ) -> x e. D )
102 100 101 syl 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> x e. D )
103 46 a1i 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> -oo e. RR* )
104 48 adantr 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> A e. RR* )
105 65 40 eqeltrd 
 |-  ( ( ph /\ x e. D ) -> ( G ` x ) e. RR )
106 105 rexrd 
 |-  ( ( ph /\ x e. D ) -> ( G ` x ) e. RR* )
107 102 106 syldan 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> ( G ` x ) e. RR* )
108 101 adantl 
 |-  ( ( ph /\ x e. ( ( H ` M ) i^i D ) ) -> x e. D )
109 108 105 syldan 
 |-  ( ( ph /\ x e. ( ( H ` M ) i^i D ) ) -> ( G ` x ) e. RR )
110 109 mnfltd 
 |-  ( ( ph /\ x e. ( ( H ` M ) i^i D ) ) -> -oo < ( G ` x ) )
111 100 110 syldan 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> -oo < ( G ` x ) )
112 102 65 syldan 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> ( G ` x ) = sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
113 nfv 
 |-  F/ n ph
114 nfcv 
 |-  F/_ n x
115 nfii1 
 |-  F/_ n |^|_ n e. Z ( ( H ` n ) i^i D )
116 114 115 nfel 
 |-  F/ n x e. |^|_ n e. Z ( ( H ` n ) i^i D )
117 113 116 nfan 
 |-  F/ n ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) )
118 simpll 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) /\ n e. Z ) -> ph )
119 simpr 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) /\ n e. Z ) -> n e. Z )
120 eliinid 
 |-  ( ( x e. |^|_ n e. Z ( ( H ` n ) i^i D ) /\ n e. Z ) -> x e. ( ( H ` n ) i^i D ) )
121 120 adantll 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) /\ n e. Z ) -> x e. ( ( H ` n ) i^i D ) )
122 elinel1 
 |-  ( x e. ( ( H ` n ) i^i D ) -> x e. ( H ` n ) )
123 122 3ad2ant3 
 |-  ( ( ph /\ n e. Z /\ x e. ( ( H ` n ) i^i D ) ) -> x e. ( H ` n ) )
124 elinel2 
 |-  ( x e. ( ( H ` n ) i^i D ) -> x e. D )
125 124 adantl 
 |-  ( ( n e. Z /\ x e. ( ( H ` n ) i^i D ) ) -> x e. D )
126 34 ancoms 
 |-  ( ( n e. Z /\ x e. D ) -> x e. dom ( F ` n ) )
127 125 126 syldan 
 |-  ( ( n e. Z /\ x e. ( ( H ` n ) i^i D ) ) -> x e. dom ( F ` n ) )
128 127 3adant1 
 |-  ( ( ph /\ n e. Z /\ x e. ( ( H ` n ) i^i D ) ) -> x e. dom ( F ` n ) )
129 123 128 elind 
 |-  ( ( ph /\ n e. Z /\ x e. ( ( H ` n ) i^i D ) ) -> x e. ( ( H ` n ) i^i dom ( F ` n ) ) )
130 9 3adant3 
 |-  ( ( ph /\ n e. Z /\ x e. ( ( H ` n ) i^i D ) ) -> ( `' ( F ` n ) " ( -oo (,] A ) ) = ( ( H ` n ) i^i dom ( F ` n ) ) )
131 129 130 eleqtrrd 
 |-  ( ( ph /\ n e. Z /\ x e. ( ( H ` n ) i^i D ) ) -> x e. ( `' ( F ` n ) " ( -oo (,] A ) ) )
132 46 a1i 
 |-  ( ( ph /\ n e. Z /\ x e. ( `' ( F ` n ) " ( -oo (,] A ) ) ) -> -oo e. RR* )
133 48 3ad2ant1 
 |-  ( ( ph /\ n e. Z /\ x e. ( `' ( F ` n ) " ( -oo (,] A ) ) ) -> A e. RR* )
134 simp3 
 |-  ( ( ph /\ n e. Z /\ x e. ( `' ( F ` n ) " ( -oo (,] A ) ) ) -> x e. ( `' ( F ` n ) " ( -oo (,] A ) ) )
135 elpreima 
 |-  ( ( F ` n ) Fn dom ( F ` n ) -> ( x e. ( `' ( F ` n ) " ( -oo (,] A ) ) <-> ( x e. dom ( F ` n ) /\ ( ( F ` n ) ` x ) e. ( -oo (,] A ) ) ) )
136 14 135 syl 
 |-  ( ( ph /\ n e. Z ) -> ( x e. ( `' ( F ` n ) " ( -oo (,] A ) ) <-> ( x e. dom ( F ` n ) /\ ( ( F ` n ) ` x ) e. ( -oo (,] A ) ) ) )
137 136 3adant3 
 |-  ( ( ph /\ n e. Z /\ x e. ( `' ( F ` n ) " ( -oo (,] A ) ) ) -> ( x e. ( `' ( F ` n ) " ( -oo (,] A ) ) <-> ( x e. dom ( F ` n ) /\ ( ( F ` n ) ` x ) e. ( -oo (,] A ) ) ) )
138 134 137 mpbid 
 |-  ( ( ph /\ n e. Z /\ x e. ( `' ( F ` n ) " ( -oo (,] A ) ) ) -> ( x e. dom ( F ` n ) /\ ( ( F ` n ) ` x ) e. ( -oo (,] A ) ) )
139 138 simprd 
 |-  ( ( ph /\ n e. Z /\ x e. ( `' ( F ` n ) " ( -oo (,] A ) ) ) -> ( ( F ` n ) ` x ) e. ( -oo (,] A ) )
140 132 133 139 iocleubd 
 |-  ( ( ph /\ n e. Z /\ x e. ( `' ( F ` n ) " ( -oo (,] A ) ) ) -> ( ( F ` n ) ` x ) <_ A )
141 131 140 syld3an3 
 |-  ( ( ph /\ n e. Z /\ x e. ( ( H ` n ) i^i D ) ) -> ( ( F ` n ) ` x ) <_ A )
142 118 119 121 141 syl3anc 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) /\ n e. Z ) -> ( ( F ` n ) ` x ) <_ A )
143 142 ex 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> ( n e. Z -> ( ( F ` n ) ` x ) <_ A ) )
144 117 143 ralrimi 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> A. n e. Z ( ( F ` n ) ` x ) <_ A )
145 28 adantr 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> Z =/= (/) )
146 102 36 syldanl 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR )
147 102 38 syl 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y )
148 7 adantr 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> A e. RR )
149 117 145 146 147 148 suprleubrnmpt 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> ( sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) <_ A <-> A. n e. Z ( ( F ` n ) ` x ) <_ A ) )
150 144 149 mpbird 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> sup ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) <_ A )
151 112 150 eqbrtrd 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> ( G ` x ) <_ A )
152 103 104 107 111 151 eliocd 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> ( G ` x ) e. ( -oo (,] A ) )
153 94 102 152 elpreimad 
 |-  ( ( ph /\ x e. |^|_ n e. Z ( ( H ` n ) i^i D ) ) -> x e. ( `' G " ( -oo (,] A ) ) )
154 153 ssd 
 |-  ( ph -> |^|_ n e. Z ( ( H ` n ) i^i D ) C_ ( `' G " ( -oo (,] A ) ) )
155 93 154 eqsstrd 
 |-  ( ph -> ( |^|_ n e. Z ( H ` n ) i^i D ) C_ ( `' G " ( -oo (,] A ) ) )
156 91 155 eqssd 
 |-  ( ph -> ( `' G " ( -oo (,] A ) ) = ( |^|_ n e. Z ( H ` n ) i^i D ) )
157 eqid 
 |-  { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y }
158 fvex 
 |-  ( F ` n ) e. _V
159 158 dmex 
 |-  dom ( F ` n ) e. _V
160 159 rgenw 
 |-  A. n e. Z dom ( F ` n ) e. _V
161 160 a1i 
 |-  ( ph -> A. n e. Z dom ( F ` n ) e. _V )
162 28 161 iinexd 
 |-  ( ph -> |^|_ n e. Z dom ( F ` n ) e. _V )
163 157 162 rabexd 
 |-  ( ph -> { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z ( ( F ` n ) ` x ) <_ y } e. _V )
164 5 163 eqeltrid 
 |-  ( ph -> D e. _V )
165 2 uzct 
 |-  Z ~<_ _om
166 165 a1i 
 |-  ( ph -> Z ~<_ _om )
167 8 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) e. S )
168 3 166 28 167 saliincl 
 |-  ( ph -> |^|_ n e. Z ( H ` n ) e. S )
169 eqid 
 |-  ( |^|_ n e. Z ( H ` n ) i^i D ) = ( |^|_ n e. Z ( H ` n ) i^i D )
170 3 164 168 169 elrestd 
 |-  ( ph -> ( |^|_ n e. Z ( H ` n ) i^i D ) e. ( S |`t D ) )
171 156 170 eqeltrd 
 |-  ( ph -> ( `' G " ( -oo (,] A ) ) e. ( S |`t D ) )