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 ffvelrnda
 |-  ( ( 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 ffvelrnd
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR )
37 5 rabeq2i
 |-  ( 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 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( 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 ) )