Metamath Proof Explorer

Theorem smfliminflem

Description: The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses smfliminflem.m 
|- ( ph -> M e. ZZ )
smfliminflem.z 
|- Z = ( ZZ>= ` M )
smfliminflem.s 
|- ( ph -> S e. SAlg )
smfliminflem.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smfliminflem.d 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
smfliminflem.g 
|- G = ( x e. D |-> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
Assertion smfliminflem 
|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfliminflem.m 
 |-  ( ph -> M e. ZZ )
2 smfliminflem.z 
 |-  Z = ( ZZ>= ` M )
3 smfliminflem.s 
 |-  ( ph -> S e. SAlg )
4 smfliminflem.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
5 smfliminflem.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR }
6 smfliminflem.g 
 |-  G = ( x e. D |-> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
7 6 a1i 
 |-  ( ph -> G = ( x e. D |-> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) )
8 ssrab2 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
9 5 8 eqsstri 
 |-  D C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
10 id 
 |-  ( x e. D -> x e. D )
11 9 10 sselid 
 |-  ( x e. D -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
12 eqid 
 |-  U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
13 2 12 allbutfi 
 |-  ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> E. n e. Z A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) )
14 11 13 sylib 
 |-  ( x e. D -> E. n e. Z A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) )
15 14 adantl 
 |-  ( ( ph /\ x e. D ) -> E. n e. Z A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) )
16 nfv 
 |-  F/ m ( ph /\ n e. Z )
17 nfra1 
 |-  F/ m A. m e. ( ZZ>= ` n ) x e. dom ( F ` m )
18 16 17 nfan 
 |-  F/ m ( ( ph /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) )
19 2 fvexi 
 |-  Z e. _V
20 19 a1i 
 |-  ( ( ( ph /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) ) -> Z e. _V )
21 2 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
22 21 zred 
 |-  ( n e. Z -> n e. RR )
23 22 ad2antlr 
 |-  ( ( ( ph /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) ) -> n e. RR )
24 simpll 
 |-  ( ( ( ph /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) ) -> ph )
25 elinel1 
 |-  ( m e. ( Z i^i ( n [,) +oo ) ) -> m e. Z )
26 3 adantr 
 |-  ( ( ph /\ m e. Z ) -> S e. SAlg )
27 4 ffvelcdmda 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
28 eqid 
 |-  dom ( F ` m ) = dom ( F ` m )
29 26 27 28 smff 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
30 24 25 29 syl2an 
 |-  ( ( ( ( ph /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) ) /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> ( F ` m ) : dom ( F ` m ) --> RR )
31 simplr 
 |-  ( ( ( n e. Z /\ A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) ) /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) )
32 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
33 21 adantr 
 |-  ( ( n e. Z /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> n e. ZZ )
34 2 25 eluzelz2d 
 |-  ( m e. ( Z i^i ( n [,) +oo ) ) -> m e. ZZ )
35 34 adantl 
 |-  ( ( n e. Z /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> m e. ZZ )
36 22 rexrd 
 |-  ( n e. Z -> n e. RR* )
37 36 adantr 
 |-  ( ( n e. Z /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> n e. RR* )
38 pnfxr 
 |-  +oo e. RR*
39 38 a1i 
 |-  ( ( n e. Z /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> +oo e. RR* )
40 elinel2 
 |-  ( m e. ( Z i^i ( n [,) +oo ) ) -> m e. ( n [,) +oo ) )
41 40 adantl 
 |-  ( ( n e. Z /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> m e. ( n [,) +oo ) )
42 37 39 41 icogelbd 
 |-  ( ( n e. Z /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> n <_ m )
43 32 33 35 42 eluzd 
 |-  ( ( n e. Z /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> m e. ( ZZ>= ` n ) )
44 43 adantlr 
 |-  ( ( ( n e. Z /\ A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) ) /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> m e. ( ZZ>= ` n ) )
45 rspa 
 |-  ( ( A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) /\ m e. ( ZZ>= ` n ) ) -> x e. dom ( F ` m ) )
46 31 44 45 syl2anc 
 |-  ( ( ( n e. Z /\ A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) ) /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> x e. dom ( F ` m ) )
47 46 adantlll 
 |-  ( ( ( ( ph /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) ) /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> x e. dom ( F ` m ) )
48 30 47 ffvelcdmd 
 |-  ( ( ( ( ph /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) ) /\ m e. ( Z i^i ( n [,) +oo ) ) ) -> ( ( F ` m ) ` x ) e. RR )
49 18 20 23 48 liminfval4 
 |-  ( ( ( ph /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) ) -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) )
50 49 rexlimdva2 
 |-  ( ph -> ( E. n e. Z A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) ) )
51 50 adantr 
 |-  ( ( ph /\ x e. D ) -> ( E. n e. Z A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) ) )
52 15 51 mpd 
 |-  ( ( ph /\ x e. D ) -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) )
53 52 xnegeqd 
 |-  ( ( ph /\ x e. D ) -> -e ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) )
54 19 mptex 
 |-  ( m e. Z |-> -u ( ( F ` m ) ` x ) ) e. _V
55 54 limsupcli 
 |-  ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR*
56 55 xnegnegi 
 |-  -e -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) )
57 56 a1i 
 |-  ( ( ph /\ x e. D ) -> -e -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) )
58 53 57 eqtr2d 
 |-  ( ( ph /\ x e. D ) -> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) = -e ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
59 5 reqabi 
 |-  ( x e. D <-> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) )
60 59 simprbi 
 |-  ( x e. D -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
61 60 adantl 
 |-  ( ( ph /\ x e. D ) -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
62 61 rexnegd 
 |-  ( ( ph /\ x e. D ) -> -e ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -u ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
63 58 62 eqtr2d 
 |-  ( ( ph /\ x e. D ) -> -u ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) )
64 61 renegcld 
 |-  ( ( ph /\ x e. D ) -> -u ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
65 63 64 eqeltrrd 
 |-  ( ( ph /\ x e. D ) -> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR )
66 65 rexnegd 
 |-  ( ( ph /\ x e. D ) -> -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) = -u ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) )
67 52 66 eqtrd 
 |-  ( ( ph /\ x e. D ) -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -u ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) )
68 67 mpteq2dva 
 |-  ( ph -> ( x e. D |-> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) = ( x e. D |-> -u ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) ) )
69 7 68 eqtrd 
 |-  ( ph -> G = ( x e. D |-> -u ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) ) )
70 nfv 
 |-  F/ x ph
71 21 32 uzn0d 
 |-  ( n e. Z -> ( ZZ>= ` n ) =/= (/) )
72 fvex 
 |-  ( F ` m ) e. _V
73 72 dmex 
 |-  dom ( F ` m ) e. _V
74 73 rgenw 
 |-  A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V
75 74 a1i 
 |-  ( n e. Z -> A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
76 iinexg 
 |-  ( ( ( ZZ>= ` n ) =/= (/) /\ A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
77 71 75 76 syl2anc 
 |-  ( n e. Z -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
78 77 rgen 
 |-  A. n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V
79 iunexg 
 |-  ( ( Z e. _V /\ A. n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V ) -> U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
80 19 78 79 mp2an 
 |-  U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V
81 80 9 ssexi 
 |-  D e. _V
82 81 a1i 
 |-  ( ph -> D e. _V )
83 5 a1i 
 |-  ( ph -> D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } )
84 13 biimpi 
 |-  ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> E. n e. Z A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) )
85 50 imp 
 |-  ( ( ph /\ E. n e. Z A. m e. ( ZZ>= ` n ) x e. dom ( F ` m ) ) -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) )
86 84 85 sylan2 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) )
87 55 a1i 
 |-  ( ( ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) /\ ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) -> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR* )
88 simpl 
 |-  ( ( ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) /\ ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) )
89 simpr 
 |-  ( ( ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) /\ ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
90 88 89 eqeltrrd 
 |-  ( ( ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) /\ ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) -> -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR )
91 xnegrecl2 
 |-  ( ( ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR* /\ -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR ) -> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR )
92 87 90 91 syl2anc 
 |-  ( ( ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) /\ ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR ) -> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR )
93 simpl 
 |-  ( ( ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) /\ ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR ) -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) )
94 xnegrecl 
 |-  ( ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR -> -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR )
95 94 adantl 
 |-  ( ( ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) /\ ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR ) -> -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR )
96 93 95 eqeltrd 
 |-  ( ( ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) /\ ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR ) -> ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
97 92 96 impbida 
 |-  ( ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = -e ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) -> ( ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR <-> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR ) )
98 86 97 syl 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR <-> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR ) )
99 98 rabbidva 
 |-  ( ph -> { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( liminf ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR } = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR } )
100 83 99 eqtrd 
 |-  ( ph -> D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR } )
101 70 100 mpteq1df 
 |-  ( ph -> ( x e. D |-> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) ) = ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR } |-> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) ) )
102 nfv 
 |-  F/ m ph
103 nfv 
 |-  F/ n ph
104 negex 
 |-  -u ( ( F ` m ) ` x ) e. _V
105 104 a1i 
 |-  ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> -u ( ( F ` m ) ` x ) e. _V )
106 nfv 
 |-  F/ x ( ph /\ m e. Z )
107 73 a1i 
 |-  ( ( ph /\ m e. Z ) -> dom ( F ` m ) e. _V )
108 29 ffvelcdmda 
 |-  ( ( ( ph /\ m e. Z ) /\ x e. dom ( F ` m ) ) -> ( ( F ` m ) ` x ) e. RR )
109 29 feqmptd 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) = ( x e. dom ( F ` m ) |-> ( ( F ` m ) ` x ) ) )
110 109 27 eqeltrrd 
 |-  ( ( ph /\ m e. Z ) -> ( x e. dom ( F ` m ) |-> ( ( F ` m ) ` x ) ) e. ( SMblFn ` S ) )
111 106 26 107 108 110 smfneg 
 |-  ( ( ph /\ m e. Z ) -> ( x e. dom ( F ` m ) |-> -u ( ( F ` m ) ` x ) ) e. ( SMblFn ` S ) )
112 eqid 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR } = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR }
113 eqid 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR } |-> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) ) = ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR } |-> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) )
114 102 70 103 1 2 3 105 111 112 113 smflimsupmpt 
 |-  ( ph -> ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) e. RR } |-> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) ) e. ( SMblFn ` S ) )
115 101 114 eqeltrd 
 |-  ( ph -> ( x e. D |-> ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) ) e. ( SMblFn ` S ) )
116 70 3 82 65 115 smfneg 
 |-  ( ph -> ( x e. D |-> -u ( limsup ` ( m e. Z |-> -u ( ( F ` m ) ` x ) ) ) ) e. ( SMblFn ` S ) )
117 69 116 eqeltrd 
 |-  ( ph -> G e. ( SMblFn ` S ) )