Metamath Proof Explorer

Theorem smfinflem

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

Ref Expression
Hypotheses smfinflem.m 
|- ( ph -> M e. ZZ )
smfinflem.z 
|- Z = ( ZZ>= ` M )
smfinflem.s 
|- ( ph -> S e. SAlg )
smfinflem.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smfinflem.d 
|- D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) }
smfinflem.g 
|- G = ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
Assertion smfinflem 
|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfinflem.m 
 |-  ( ph -> M e. ZZ )
2 smfinflem.z 
 |-  Z = ( ZZ>= ` M )
3 smfinflem.s 
 |-  ( ph -> S e. SAlg )
4 smfinflem.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
5 smfinflem.d 
 |-  D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) }
6 smfinflem.g 
 |-  G = ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) )
7 6 a1i 
 |-  ( ph -> G = ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) )
8 nfv 
 |-  F/ n ( ph /\ x e. D )
9 1 2 uzn0d 
 |-  ( ph -> Z =/= (/) )
10 9 adantr 
 |-  ( ( ph /\ x e. D ) -> Z =/= (/) )
11 3 adantr 
 |-  ( ( ph /\ n e. Z ) -> S e. SAlg )
12 4 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. ( SMblFn ` S ) )
13 eqid 
 |-  dom ( F ` n ) = dom ( F ` n )
14 11 12 13 smff 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR )
15 14 adantlr 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ( F ` n ) : dom ( F ` n ) --> RR )
16 ssrab2 
 |-  { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } C_ |^|_ n e. Z dom ( F ` n )
17 5 eleq2i 
 |-  ( x e. D <-> x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } )
18 17 biimpi 
 |-  ( x e. D -> x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } )
19 16 18 sselid 
 |-  ( x e. D -> x e. |^|_ n e. Z dom ( F ` n ) )
20 19 adantr 
 |-  ( ( x e. D /\ n e. Z ) -> x e. |^|_ n e. Z dom ( F ` n ) )
21 simpr 
 |-  ( ( x e. D /\ n e. Z ) -> n e. Z )
22 eliinid 
 |-  ( ( x e. |^|_ n e. Z dom ( F ` n ) /\ n e. Z ) -> x e. dom ( F ` n ) )
23 20 21 22 syl2anc 
 |-  ( ( x e. D /\ n e. Z ) -> x e. dom ( F ` n ) )
24 23 adantll 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> x e. dom ( F ` n ) )
25 15 24 ffvelrnd 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR )
26 rabidim2 
 |-  ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) )
27 18 26 syl 
 |-  ( x e. D -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) )
28 27 adantl 
 |-  ( ( ph /\ x e. D ) -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) )
29 8 10 25 28 infnsuprnmpt 
 |-  ( ( ph /\ x e. D ) -> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) = -u sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) )
30 29 mpteq2dva 
 |-  ( ph -> ( x e. D |-> inf ( ran ( n e. Z |-> ( ( F ` n ) ` x ) ) , RR , < ) ) = ( x e. D |-> -u sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) )
31 7 30 eqtrd 
 |-  ( ph -> G = ( x e. D |-> -u sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) )
32 nfv 
 |-  F/ x ph
33 fvex 
 |-  ( F ` n ) e. _V
34 33 dmex 
 |-  dom ( F ` n ) e. _V
35 34 rgenw 
 |-  A. n e. Z dom ( F ` n ) e. _V
36 35 a1i 
 |-  ( ph -> A. n e. Z dom ( F ` n ) e. _V )
37 9 36 iinexd 
 |-  ( ph -> |^|_ n e. Z dom ( F ` n ) e. _V )
38 5 37 rabexd 
 |-  ( ph -> D e. _V )
39 25 renegcld 
 |-  ( ( ( ph /\ x e. D ) /\ n e. Z ) -> -u ( ( F ` n ) ` x ) e. RR )
40 fveq2 
 |-  ( w = x -> ( ( F ` m ) ` w ) = ( ( F ` m ) ` x ) )
41 40 breq2d 
 |-  ( w = x -> ( z <_ ( ( F ` m ) ` w ) <-> z <_ ( ( F ` m ) ` x ) ) )
42 41 ralbidv 
 |-  ( w = x -> ( A. m e. Z z <_ ( ( F ` m ) ` w ) <-> A. m e. Z z <_ ( ( F ` m ) ` x ) ) )
43 42 rexbidv 
 |-  ( w = x -> ( E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) <-> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` x ) ) )
44 nfcv 
 |-  F/_ w |^|_ n e. Z dom ( F ` n )
45 nfcv 
 |-  F/_ x Z
46 nfcv 
 |-  F/_ x ( F ` m )
47 46 nfdm 
 |-  F/_ x dom ( F ` m )
48 45 47 nfiin 
 |-  F/_ x |^|_ m e. Z dom ( F ` m )
49 nfv 
 |-  F/ w E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x )
50 nfv 
 |-  F/ x E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w )
51 nfcv 
 |-  F/_ m dom ( F ` n )
52 nfcv 
 |-  F/_ n ( F ` m )
53 52 nfdm 
 |-  F/_ n dom ( F ` m )
54 fveq2 
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
55 54 dmeqd 
 |-  ( n = m -> dom ( F ` n ) = dom ( F ` m ) )
56 51 53 55 cbviin 
 |-  |^|_ n e. Z dom ( F ` n ) = |^|_ m e. Z dom ( F ` m )
57 56 a1i 
 |-  ( x = w -> |^|_ n e. Z dom ( F ` n ) = |^|_ m e. Z dom ( F ` m ) )
58 fveq2 
 |-  ( x = w -> ( ( F ` n ) ` x ) = ( ( F ` n ) ` w ) )
59 58 breq2d 
 |-  ( x = w -> ( y <_ ( ( F ` n ) ` x ) <-> y <_ ( ( F ` n ) ` w ) ) )
60 59 ralbidv 
 |-  ( x = w -> ( A. n e. Z y <_ ( ( F ` n ) ` x ) <-> A. n e. Z y <_ ( ( F ` n ) ` w ) ) )
61 nfv 
 |-  F/ m y <_ ( ( F ` n ) ` w )
62 nfcv 
 |-  F/_ n y
63 nfcv 
 |-  F/_ n <_
64 nfcv 
 |-  F/_ n w
65 52 64 nffv 
 |-  F/_ n ( ( F ` m ) ` w )
66 62 63 65 nfbr 
 |-  F/ n y <_ ( ( F ` m ) ` w )
67 54 fveq1d 
 |-  ( n = m -> ( ( F ` n ) ` w ) = ( ( F ` m ) ` w ) )
68 67 breq2d 
 |-  ( n = m -> ( y <_ ( ( F ` n ) ` w ) <-> y <_ ( ( F ` m ) ` w ) ) )
69 61 66 68 cbvralw 
 |-  ( A. n e. Z y <_ ( ( F ` n ) ` w ) <-> A. m e. Z y <_ ( ( F ` m ) ` w ) )
70 69 a1i 
 |-  ( x = w -> ( A. n e. Z y <_ ( ( F ` n ) ` w ) <-> A. m e. Z y <_ ( ( F ` m ) ` w ) ) )
71 60 70 bitrd 
 |-  ( x = w -> ( A. n e. Z y <_ ( ( F ` n ) ` x ) <-> A. m e. Z y <_ ( ( F ` m ) ` w ) ) )
72 71 rexbidv 
 |-  ( x = w -> ( E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) <-> E. y e. RR A. m e. Z y <_ ( ( F ` m ) ` w ) ) )
73 breq1 
 |-  ( y = z -> ( y <_ ( ( F ` m ) ` w ) <-> z <_ ( ( F ` m ) ` w ) ) )
74 73 ralbidv 
 |-  ( y = z -> ( A. m e. Z y <_ ( ( F ` m ) ` w ) <-> A. m e. Z z <_ ( ( F ` m ) ` w ) ) )
75 74 cbvrexvw 
 |-  ( E. y e. RR A. m e. Z y <_ ( ( F ` m ) ` w ) <-> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) )
76 75 a1i 
 |-  ( x = w -> ( E. y e. RR A. m e. Z y <_ ( ( F ` m ) ` w ) <-> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) ) )
77 72 76 bitrd 
 |-  ( x = w -> ( E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) <-> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) ) )
78 44 48 49 50 57 77 cbvrabcsfw 
 |-  { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } = { w e. |^|_ m e. Z dom ( F ` m ) | E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) }
79 5 78 eqtri 
 |-  D = { w e. |^|_ m e. Z dom ( F ` m ) | E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` w ) }
80 43 79 elrab2 
 |-  ( x e. D <-> ( x e. |^|_ m e. Z dom ( F ` m ) /\ E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` x ) ) )
81 80 biimpi 
 |-  ( x e. D -> ( x e. |^|_ m e. Z dom ( F ` m ) /\ E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` x ) ) )
82 81 simprd 
 |-  ( x e. D -> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` x ) )
83 82 adantl 
 |-  ( ( ph /\ x e. D ) -> E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` x ) )
84 renegcl 
 |-  ( z e. RR -> -u z e. RR )
85 84 ad2antlr 
 |-  ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) -> -u z e. RR )
86 fveq2 
 |-  ( m = n -> ( F ` m ) = ( F ` n ) )
87 86 fveq1d 
 |-  ( m = n -> ( ( F ` m ) ` x ) = ( ( F ` n ) ` x ) )
88 87 breq2d 
 |-  ( m = n -> ( z <_ ( ( F ` m ) ` x ) <-> z <_ ( ( F ` n ) ` x ) ) )
89 88 rspcva 
 |-  ( ( n e. Z /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) -> z <_ ( ( F ` n ) ` x ) )
90 89 ancoms 
 |-  ( ( A. m e. Z z <_ ( ( F ` m ) ` x ) /\ n e. Z ) -> z <_ ( ( F ` n ) ` x ) )
91 90 adantll 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) /\ n e. Z ) -> z <_ ( ( F ` n ) ` x ) )
92 simpllr 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) /\ n e. Z ) -> z e. RR )
93 25 ad4ant14 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR )
94 92 93 lenegd 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) /\ n e. Z ) -> ( z <_ ( ( F ` n ) ` x ) <-> -u ( ( F ` n ) ` x ) <_ -u z ) )
95 91 94 mpbid 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) /\ n e. Z ) -> -u ( ( F ` n ) ` x ) <_ -u z )
96 95 ralrimiva 
 |-  ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) -> A. n e. Z -u ( ( F ` n ) ` x ) <_ -u z )
97 brralrspcev 
 |-  ( ( -u z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ -u z ) -> E. y e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ y )
98 85 96 97 syl2anc 
 |-  ( ( ( ( ph /\ x e. D ) /\ z e. RR ) /\ A. m e. Z z <_ ( ( F ` m ) ` x ) ) -> E. y e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ y )
99 98 rexlimdva2 
 |-  ( ( ph /\ x e. D ) -> ( E. z e. RR A. m e. Z z <_ ( ( F ` m ) ` x ) -> E. y e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ y ) )
100 83 99 mpd 
 |-  ( ( ph /\ x e. D ) -> E. y e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ y )
101 8 10 39 100 suprclrnmpt 
 |-  ( ( ph /\ x e. D ) -> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) e. RR )
102 5 a1i 
 |-  ( ph -> D = { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } )
103 nfv 
 |-  F/ y ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) )
104 nfv 
 |-  F/ y E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z
105 renegcl 
 |-  ( y e. RR -> -u y e. RR )
106 105 3ad2ant2 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) -> -u y e. RR )
107 nfv 
 |-  F/ n ph
108 nfcv 
 |-  F/_ n x
109 nfii1 
 |-  F/_ n |^|_ n e. Z dom ( F ` n )
110 108 109 nfel 
 |-  F/ n x e. |^|_ n e. Z dom ( F ` n )
111 107 110 nfan 
 |-  F/ n ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) )
112 62 nfel1 
 |-  F/ n y e. RR
113 nfra1 
 |-  F/ n A. n e. Z y <_ ( ( F ` n ) ` x )
114 111 112 113 nf3an 
 |-  F/ n ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) )
115 simpl2 
 |-  ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) /\ n e. Z ) -> y e. RR )
116 simpll 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ n e. Z ) -> ph )
117 simpr 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ n e. Z ) -> n e. Z )
118 22 adantll 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ n e. Z ) -> x e. dom ( F ` n ) )
119 14 3adant3 
 |-  ( ( ph /\ n e. Z /\ x e. dom ( F ` n ) ) -> ( F ` n ) : dom ( F ` n ) --> RR )
120 simp3 
 |-  ( ( ph /\ n e. Z /\ x e. dom ( F ` n ) ) -> x e. dom ( F ` n ) )
121 119 120 ffvelrnd 
 |-  ( ( ph /\ n e. Z /\ x e. dom ( F ` n ) ) -> ( ( F ` n ) ` x ) e. RR )
122 116 117 118 121 syl3anc 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR )
123 122 3ad2antl1 
 |-  ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR )
124 rspa 
 |-  ( ( A. n e. Z y <_ ( ( F ` n ) ` x ) /\ n e. Z ) -> y <_ ( ( F ` n ) ` x ) )
125 124 3ad2antl3 
 |-  ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) /\ n e. Z ) -> y <_ ( ( F ` n ) ` x ) )
126 leneg 
 |-  ( ( y e. RR /\ ( ( F ` n ) ` x ) e. RR ) -> ( y <_ ( ( F ` n ) ` x ) <-> -u ( ( F ` n ) ` x ) <_ -u y ) )
127 126 biimp3a 
 |-  ( ( y e. RR /\ ( ( F ` n ) ` x ) e. RR /\ y <_ ( ( F ` n ) ` x ) ) -> -u ( ( F ` n ) ` x ) <_ -u y )
128 115 123 125 127 syl3anc 
 |-  ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) /\ n e. Z ) -> -u ( ( F ` n ) ` x ) <_ -u y )
129 128 ex 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) -> ( n e. Z -> -u ( ( F ` n ) ` x ) <_ -u y ) )
130 114 129 ralrimi 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) -> A. n e. Z -u ( ( F ` n ) ` x ) <_ -u y )
131 brralrspcev 
 |-  ( ( -u y e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ -u y ) -> E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z )
132 106 130 131 syl2anc 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ y e. RR /\ A. n e. Z y <_ ( ( F ` n ) ` x ) ) -> E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z )
133 132 3exp 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> ( y e. RR -> ( A. n e. Z y <_ ( ( F ` n ) ` x ) -> E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) ) )
134 103 104 133 rexlimd 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> ( E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) -> E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) )
135 84 3ad2ant2 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) -> -u z e. RR )
136 nfv 
 |-  F/ n z e. RR
137 nfra1 
 |-  F/ n A. n e. Z -u ( ( F ` n ) ` x ) <_ z
138 111 136 137 nf3an 
 |-  F/ n ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z )
139 122 3ad2antl1 
 |-  ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) /\ n e. Z ) -> ( ( F ` n ) ` x ) e. RR )
140 simpl2 
 |-  ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) /\ n e. Z ) -> z e. RR )
141 rspa 
 |-  ( ( A. n e. Z -u ( ( F ` n ) ` x ) <_ z /\ n e. Z ) -> -u ( ( F ` n ) ` x ) <_ z )
142 141 3ad2antl3 
 |-  ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) /\ n e. Z ) -> -u ( ( F ` n ) ` x ) <_ z )
143 simp3 
 |-  ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR /\ -u ( ( F ` n ) ` x ) <_ z ) -> -u ( ( F ` n ) ` x ) <_ z )
144 renegcl 
 |-  ( ( ( F ` n ) ` x ) e. RR -> -u ( ( F ` n ) ` x ) e. RR )
145 144 adantr 
 |-  ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR ) -> -u ( ( F ` n ) ` x ) e. RR )
146 simpr 
 |-  ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR ) -> z e. RR )
147 leneg 
 |-  ( ( -u ( ( F ` n ) ` x ) e. RR /\ z e. RR ) -> ( -u ( ( F ` n ) ` x ) <_ z <-> -u z <_ -u -u ( ( F ` n ) ` x ) ) )
148 145 146 147 syl2anc 
 |-  ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR ) -> ( -u ( ( F ` n ) ` x ) <_ z <-> -u z <_ -u -u ( ( F ` n ) ` x ) ) )
149 148 3adant3 
 |-  ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR /\ -u ( ( F ` n ) ` x ) <_ z ) -> ( -u ( ( F ` n ) ` x ) <_ z <-> -u z <_ -u -u ( ( F ` n ) ` x ) ) )
150 143 149 mpbid 
 |-  ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR /\ -u ( ( F ` n ) ` x ) <_ z ) -> -u z <_ -u -u ( ( F ` n ) ` x ) )
151 recn 
 |-  ( ( ( F ` n ) ` x ) e. RR -> ( ( F ` n ) ` x ) e. CC )
152 151 negnegd 
 |-  ( ( ( F ` n ) ` x ) e. RR -> -u -u ( ( F ` n ) ` x ) = ( ( F ` n ) ` x ) )
153 152 3ad2ant1 
 |-  ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR /\ -u ( ( F ` n ) ` x ) <_ z ) -> -u -u ( ( F ` n ) ` x ) = ( ( F ` n ) ` x ) )
154 150 153 breqtrd 
 |-  ( ( ( ( F ` n ) ` x ) e. RR /\ z e. RR /\ -u ( ( F ` n ) ` x ) <_ z ) -> -u z <_ ( ( F ` n ) ` x ) )
155 139 140 142 154 syl3anc 
 |-  ( ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) /\ n e. Z ) -> -u z <_ ( ( F ` n ) ` x ) )
156 155 ex 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) -> ( n e. Z -> -u z <_ ( ( F ` n ) ` x ) ) )
157 138 156 ralrimi 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) -> A. n e. Z -u z <_ ( ( F ` n ) ` x ) )
158 breq1 
 |-  ( y = -u z -> ( y <_ ( ( F ` n ) ` x ) <-> -u z <_ ( ( F ` n ) ` x ) ) )
159 158 ralbidv 
 |-  ( y = -u z -> ( A. n e. Z y <_ ( ( F ` n ) ` x ) <-> A. n e. Z -u z <_ ( ( F ` n ) ` x ) ) )
160 159 rspcev 
 |-  ( ( -u z e. RR /\ A. n e. Z -u z <_ ( ( F ` n ) ` x ) ) -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) )
161 135 157 160 syl2anc 
 |-  ( ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) /\ z e. RR /\ A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) )
162 161 3exp 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> ( z e. RR -> ( A. n e. Z -u ( ( F ` n ) ` x ) <_ z -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) ) ) )
163 162 rexlimdv 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> ( E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z -> E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) ) )
164 134 163 impbid 
 |-  ( ( ph /\ x e. |^|_ n e. Z dom ( F ` n ) ) -> ( E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) <-> E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z ) )
165 32 164 rabbida 
 |-  ( ph -> { x e. |^|_ n e. Z dom ( F ` n ) | E. y e. RR A. n e. Z y <_ ( ( F ` n ) ` x ) } = { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } )
166 102 165 eqtrd 
 |-  ( ph -> D = { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } )
167 32 166 alrimi 
 |-  ( ph -> A. x D = { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } )
168 eqid 
 |-  sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) = sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < )
169 168 rgenw 
 |-  A. x e. D sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) = sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < )
170 169 a1i 
 |-  ( ph -> A. x e. D sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) = sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) )
171 mpteq12f 
 |-  ( ( A. x D = { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } /\ A. x e. D sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) = sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) -> ( x e. D |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) )
172 167 170 171 syl2anc 
 |-  ( ph -> ( x e. D |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) )
173 nfv 
 |-  F/ z ph
174 121 renegcld 
 |-  ( ( ph /\ n e. Z /\ x e. dom ( F ` n ) ) -> -u ( ( F ` n ) ` x ) e. RR )
175 nfv 
 |-  F/ x ( ph /\ n e. Z )
176 34 a1i 
 |-  ( ( ph /\ n e. Z ) -> dom ( F ` n ) e. _V )
177 121 3expa 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. dom ( F ` n ) ) -> ( ( F ` n ) ` x ) e. RR )
178 14 feqmptd 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) = ( x e. dom ( F ` n ) |-> ( ( F ` n ) ` x ) ) )
179 178 eqcomd 
 |-  ( ( ph /\ n e. Z ) -> ( x e. dom ( F ` n ) |-> ( ( F ` n ) ` x ) ) = ( F ` n ) )
180 179 12 eqeltrd 
 |-  ( ( ph /\ n e. Z ) -> ( x e. dom ( F ` n ) |-> ( ( F ` n ) ` x ) ) e. ( SMblFn ` S ) )
181 175 11 176 177 180 smfneg 
 |-  ( ( ph /\ n e. Z ) -> ( x e. dom ( F ` n ) |-> -u ( ( F ` n ) ` x ) ) e. ( SMblFn ` S ) )
182 eqid 
 |-  { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } = { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z }
183 eqid 
 |-  ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) = ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) )
184 107 32 173 1 2 3 174 181 182 183 smfsupmpt 
 |-  ( ph -> ( x e. { x e. |^|_ n e. Z dom ( F ` n ) | E. z e. RR A. n e. Z -u ( ( F ` n ) ` x ) <_ z } |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) e. ( SMblFn ` S ) )
185 172 184 eqeltrd 
 |-  ( ph -> ( x e. D |-> sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) e. ( SMblFn ` S ) )
186 32 3 38 101 185 smfneg 
 |-  ( ph -> ( x e. D |-> -u sup ( ran ( n e. Z |-> -u ( ( F ` n ) ` x ) ) , RR , < ) ) e. ( SMblFn ` S ) )
187 31 186 eqeltrd 
 |-  ( ph -> G e. ( SMblFn ` S ) )