Metamath Proof Explorer

Theorem smflimsupmpt

Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of Fremlin1 p. 39 . A can contain m as a free variable, in other words it can be thought of as an indexed collection A ( m ) . B can be thought of as a collection with two indices B ( m , x ) . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsupmpt.p 
|- F/ m ph
smflimsupmpt.x 
|- F/ x ph
smflimsupmpt.n 
|- F/ n ph
smflimsupmpt.m 
|- ( ph -> M e. ZZ )
smflimsupmpt.z 
|- Z = ( ZZ>= ` M )
smflimsupmpt.s 
|- ( ph -> S e. SAlg )
smflimsupmpt.b 
|- ( ( ph /\ m e. Z /\ x e. A ) -> B e. W )
smflimsupmpt.f 
|- ( ( ph /\ m e. Z ) -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
smflimsupmpt.d 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( limsup ` ( m e. Z |-> B ) ) e. RR }
smflimsupmpt.g 
|- G = ( x e. D |-> ( limsup ` ( m e. Z |-> B ) ) )
Assertion smflimsupmpt 
|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smflimsupmpt.p 
 |-  F/ m ph
2 smflimsupmpt.x 
 |-  F/ x ph
3 smflimsupmpt.n 
 |-  F/ n ph
4 smflimsupmpt.m 
 |-  ( ph -> M e. ZZ )
5 smflimsupmpt.z 
 |-  Z = ( ZZ>= ` M )
6 smflimsupmpt.s 
 |-  ( ph -> S e. SAlg )
7 smflimsupmpt.b 
 |-  ( ( ph /\ m e. Z /\ x e. A ) -> B e. W )
8 smflimsupmpt.f 
 |-  ( ( ph /\ m e. Z ) -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
9 smflimsupmpt.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( limsup ` ( m e. Z |-> B ) ) e. RR }
10 smflimsupmpt.g 
 |-  G = ( x e. D |-> ( limsup ` ( m e. Z |-> B ) ) )
11 10 a1i 
 |-  ( ph -> G = ( x e. D |-> ( limsup ` ( m e. Z |-> B ) ) ) )
12 9 a1i 
 |-  ( ph -> D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( limsup ` ( m e. Z |-> B ) ) e. RR } )
13 simpr 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
14 nfv 
 |-  F/ m n e. Z
15 1 14 nfan 
 |-  F/ m ( ph /\ n e. Z )
16 simpll 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ph )
17 5 uztrn2 
 |-  ( ( n e. Z /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
18 17 adantll 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
19 simpr 
 |-  ( ( ph /\ m e. Z ) -> m e. Z )
20 8 elexd 
 |-  ( ( ph /\ m e. Z ) -> ( x e. A |-> B ) e. _V )
21 eqid 
 |-  ( m e. Z |-> ( x e. A |-> B ) ) = ( m e. Z |-> ( x e. A |-> B ) )
22 21 fvmpt2 
 |-  ( ( m e. Z /\ ( x e. A |-> B ) e. _V ) -> ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) = ( x e. A |-> B ) )
23 19 20 22 syl2anc 
 |-  ( ( ph /\ m e. Z ) -> ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) = ( x e. A |-> B ) )
24 23 dmeqd 
 |-  ( ( ph /\ m e. Z ) -> dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) = dom ( x e. A |-> B ) )
25 nfv 
 |-  F/ x m e. Z
26 2 25 nfan 
 |-  F/ x ( ph /\ m e. Z )
27 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
28 7 3expa 
 |-  ( ( ( ph /\ m e. Z ) /\ x e. A ) -> B e. W )
29 26 27 28 dmmptdf 
 |-  ( ( ph /\ m e. Z ) -> dom ( x e. A |-> B ) = A )
30 24 29 eqtr2d 
 |-  ( ( ph /\ m e. Z ) -> A = dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
31 16 18 30 syl2anc 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> A = dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
32 15 31 iineq2d 
 |-  ( ( ph /\ n e. Z ) -> |^|_ m e. ( ZZ>= ` n ) A = |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
33 3 32 iuneq2df 
 |-  ( ph -> U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
34 33 adantr 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
35 13 34 eleqtrd 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
36 35 adantrr 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> B ) ) e. RR ) ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
37 eliun 
 |-  ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A <-> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A )
38 37 bilani 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A )
39 nfv 
 |-  F/ n ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> B ) )
40 nfcv 
 |-  F/_ m x
41 nfii1 
 |-  F/_ m |^|_ m e. ( ZZ>= ` n ) A
42 40 41 nfel 
 |-  F/ m x e. |^|_ m e. ( ZZ>= ` n ) A
43 1 14 42 nf3an 
 |-  F/ m ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A )
44 23 fveq1d 
 |-  ( ( ph /\ m e. Z ) -> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) = ( ( x e. A |-> B ) ` x ) )
45 16 18 44 syl2anc 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) = ( ( x e. A |-> B ) ` x ) )
46 45 3adantl3 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) = ( ( x e. A |-> B ) ` x ) )
47 eliinid 
 |-  ( ( x e. |^|_ m e. ( ZZ>= ` n ) A /\ m e. ( ZZ>= ` n ) ) -> x e. A )
48 47 3ad2antl3 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> x e. A )
49 simpl1 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ph )
50 18 3adantl3 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
51 49 50 48 7 syl3anc 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> B e. W )
52 27 fvmpt2 
 |-  ( ( x e. A /\ B e. W ) -> ( ( x e. A |-> B ) ` x ) = B )
53 48 51 52 syl2anc 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ( ( x e. A |-> B ) ` x ) = B )
54 46 53 eqtrd 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) = B )
55 43 54 mpteq2da 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( m e. ( ZZ>= ` n ) |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) = ( m e. ( ZZ>= ` n ) |-> B ) )
56 55 fveq2d 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( limsup ` ( m e. ( ZZ>= ` n ) |-> B ) ) )
57 4 3ad2ant1 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> M e. ZZ )
58 5 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
59 58 3ad2ant2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. ZZ )
60 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
61 fvexd 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. Z ) -> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) e. _V )
62 50 61 syldan 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) e. _V )
63 43 57 59 5 60 61 62 limsupequzmpt 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( limsup ` ( m e. ( ZZ>= ` n ) |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
64 14 nfci 
 |-  F/_ m Z
65 nfcv 
 |-  F/_ m ( ZZ>= ` n )
66 simp2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. Z )
67 59 uzidd 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. ( ZZ>= ` n ) )
68 43 64 65 5 60 66 67 51 limsupequzmpt2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( limsup ` ( m e. Z |-> B ) ) = ( limsup ` ( m e. ( ZZ>= ` n ) |-> B ) ) )
69 56 63 68 3eqtr4d 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> B ) ) )
70 69 3exp 
 |-  ( ph -> ( n e. Z -> ( x e. |^|_ m e. ( ZZ>= ` n ) A -> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> B ) ) ) ) )
71 3 39 70 rexlimd 
 |-  ( ph -> ( E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A -> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> B ) ) ) )
72 71 adantr 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> ( E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A -> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> B ) ) ) )
73 38 72 mpd 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> B ) ) )
74 73 adantrr 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> B ) ) e. RR ) ) -> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> B ) ) )
75 simprr 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> B ) ) e. RR ) ) -> ( limsup ` ( m e. Z |-> B ) ) e. RR )
76 74 75 eqeltrd 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> B ) ) e. RR ) ) -> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR )
77 36 76 jca 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> B ) ) e. RR ) ) -> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) )
78 77 ex 
 |-  ( ph -> ( ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> B ) ) e. RR ) -> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) ) )
79 simpl 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) ) -> ph )
80 simpr 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
81 33 eqcomd 
 |-  ( ph -> U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
82 81 adantr 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ) -> U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
83 80 82 eleqtrd 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
84 83 adantrr 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
85 simprr 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) ) -> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR )
86 simp2 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
87 73 eqcomd 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> ( limsup ` ( m e. Z |-> B ) ) = ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
88 87 3adant3 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) -> ( limsup ` ( m e. Z |-> B ) ) = ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
89 simp3 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) -> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR )
90 88 89 eqeltrd 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) -> ( limsup ` ( m e. Z |-> B ) ) e. RR )
91 86 90 jca 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) -> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> B ) ) e. RR ) )
92 79 84 85 91 syl3anc 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) ) -> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> B ) ) e. RR ) )
93 92 ex 
 |-  ( ph -> ( ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) -> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> B ) ) e. RR ) ) )
94 78 93 impbid 
 |-  ( ph -> ( ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( limsup ` ( m e. Z |-> B ) ) e. RR ) <-> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) /\ ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) ) )
95 2 94 rabbida3 
 |-  ( ph -> { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( limsup ` ( m e. Z |-> B ) ) e. RR } = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } )
96 12 95 eqtrd 
 |-  ( ph -> D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } )
97 9 eleq2i 
 |-  ( x e. D <-> x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( limsup ` ( m e. Z |-> B ) ) e. RR } )
98 97 biimpi 
 |-  ( x e. D -> x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( limsup ` ( m e. Z |-> B ) ) e. RR } )
99 rabidim1 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( limsup ` ( m e. Z |-> B ) ) e. RR } -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
100 98 99 syl 
 |-  ( x e. D -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
101 100 87 sylan2 
 |-  ( ( ph /\ x e. D ) -> ( limsup ` ( m e. Z |-> B ) ) = ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
102 2 96 101 mpteq12da 
 |-  ( ph -> ( x e. D |-> ( limsup ` ( m e. Z |-> B ) ) ) = ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } |-> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) ) )
103 11 102 eqtrd 
 |-  ( ph -> G = ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } |-> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) ) )
104 nfmpt1 
 |-  F/_ m ( m e. Z |-> ( x e. A |-> B ) )
105 nfcv 
 |-  F/_ x Z
106 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
107 105 106 nfmpt 
 |-  F/_ x ( m e. Z |-> ( x e. A |-> B ) )
108 1 8 fmptd2f 
 |-  ( ph -> ( m e. Z |-> ( x e. A |-> B ) ) : Z --> ( SMblFn ` S ) )
109 eqid 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR }
110 eqid 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } |-> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) ) = ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } |-> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
111 104 107 4 5 6 108 109 110 smflimsup 
 |-  ( ph -> ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } |-> ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) ) e. ( SMblFn ` S ) )
112 103 111 eqeltrd 
 |-  ( ph -> G e. ( SMblFn ` S ) )