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 biimpi 
 |-  ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A )
39 38 adantl 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A )
40 nfv 
 |-  F/ n ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( limsup ` ( m e. Z |-> B ) )
41 nfcv 
 |-  F/_ m x
42 nfii1 
 |-  F/_ m |^|_ m e. ( ZZ>= ` n ) A
43 41 42 nfel 
 |-  F/ m x e. |^|_ m e. ( ZZ>= ` n ) A
44 1 14 43 nf3an 
 |-  F/ m ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A )
45 23 fveq1d 
 |-  ( ( ph /\ m e. Z ) -> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) = ( ( x e. A |-> B ) ` x ) )
46 16 18 45 syl2anc 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) = ( ( x e. A |-> B ) ` x ) )
47 46 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 ) )
48 eliinid 
 |-  ( ( x e. |^|_ m e. ( ZZ>= ` n ) A /\ m e. ( ZZ>= ` n ) ) -> x e. A )
49 48 3ad2antl3 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> x e. A )
50 simpl1 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ph )
51 18 3adantl3 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
52 50 51 49 7 syl3anc 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> B e. W )
53 27 fvmpt2 
 |-  ( ( x e. A /\ B e. W ) -> ( ( x e. A |-> B ) ` x ) = B )
54 49 52 53 syl2anc 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ( ( x e. A |-> B ) ` x ) = B )
55 47 54 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 )
56 44 55 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 ) )
57 56 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 ) ) )
58 4 3ad2ant1 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> M e. ZZ )
59 5 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
60 59 3ad2ant2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. ZZ )
61 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
62 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 )
63 51 62 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 )
64 44 58 60 5 61 62 63 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 ) ) ) )
65 14 nfci 
 |-  F/_ m Z
66 nfcv 
 |-  F/_ m ( ZZ>= ` n )
67 simp2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. Z )
68 60 uzidd 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. ( ZZ>= ` n ) )
69 44 65 66 5 61 67 68 52 limsupequzmpt2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( limsup ` ( m e. Z |-> B ) ) = ( limsup ` ( m e. ( ZZ>= ` n ) |-> B ) ) )
70 57 64 69 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 ) ) )
71 70 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 ) ) ) ) )
72 3 40 71 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 ) ) ) )
73 72 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 ) ) ) )
74 39 73 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 ) ) )
75 74 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 ) ) )
76 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 )
77 75 76 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 )
78 36 77 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 ) )
79 78 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 ) ) )
80 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 )
81 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 ) )
82 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 )
83 82 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 )
84 81 83 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 )
85 84 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 )
86 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 )
87 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 )
88 74 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 ) ) ) )
89 88 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 ) ) ) )
90 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 )
91 89 90 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 )
92 87 91 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 ) )
93 80 85 86 92 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 ) )
94 93 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 ) ) )
95 79 94 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 ) ) )
96 2 95 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 } )
97 12 96 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 } )
98 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 } )
99 98 biimpi 
 |-  ( x e. D -> x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( limsup ` ( m e. Z |-> B ) ) e. RR } )
100 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 )
101 99 100 syl 
 |-  ( x e. D -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
102 101 88 sylan2 
 |-  ( ( ph /\ x e. D ) -> ( limsup ` ( m e. Z |-> B ) ) = ( limsup ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
103 2 97 102 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 ) ) ) ) )
104 11 103 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 ) ) ) ) )
105 nfmpt1 
 |-  F/_ m ( m e. Z |-> ( x e. A |-> B ) )
106 nfcv 
 |-  F/_ x Z
107 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
108 106 107 nfmpt 
 |-  F/_ x ( m e. Z |-> ( x e. A |-> B ) )
109 1 8 fmptd2f 
 |-  ( ph -> ( m e. Z |-> ( x e. A |-> B ) ) : Z --> ( SMblFn ` S ) )
110 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 }
111 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 ) ) ) )
112 105 108 4 5 6 109 110 111 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 ) )
113 104 112 eqeltrd 
 |-  ( ph -> G e. ( SMblFn ` S ) )