Metamath Proof Explorer

Theorem smfliminfmpt

Description: The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) 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, 2-Jan-2022)

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

Proof

Step Hyp Ref Expression
1 smfliminfmpt.p 
 |-  F/ m ph
2 smfliminfmpt.x 
 |-  F/ x ph
3 smfliminfmpt.n 
 |-  F/ n ph
4 smfliminfmpt.m 
 |-  ( ph -> M e. ZZ )
5 smfliminfmpt.z 
 |-  Z = ( ZZ>= ` M )
6 smfliminfmpt.s 
 |-  ( ph -> S e. SAlg )
7 smfliminfmpt.b 
 |-  ( ( ph /\ m e. Z /\ x e. A ) -> B e. V )
8 smfliminfmpt.f 
 |-  ( ( ph /\ m e. Z ) -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
9 smfliminfmpt.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( liminf ` ( m e. Z |-> B ) ) e. RR }
10 smfliminfmpt.g 
 |-  G = ( x e. D |-> ( liminf ` ( m e. Z |-> B ) ) )
11 10 a1i 
 |-  ( ph -> G = ( x e. D |-> ( liminf ` ( m e. Z |-> B ) ) ) )
12 9 a1i 
 |-  ( ph -> D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( liminf ` ( 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. V )
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 /\ ( liminf ` ( 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 ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( liminf ` ( 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 simp2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. Z )
52 51 17 sylan 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
53 50 52 49 7 syl3anc 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> B e. V )
54 27 fvmpt2 
 |-  ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B )
55 49 53 54 syl2anc 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ( ( x e. A |-> B ) ` x ) = B )
56 47 55 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 )
57 44 56 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 ) )
58 57 fveq2d 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( liminf ` ( m e. ( ZZ>= ` n ) |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( liminf ` ( m e. ( ZZ>= ` n ) |-> B ) ) )
59 nfcv 
 |-  F/_ m Z
60 nfcv 
 |-  F/_ m ( ZZ>= ` n )
61 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
62 5 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
63 62 uzidd 
 |-  ( n e. Z -> n e. ( ZZ>= ` n ) )
64 63 3ad2ant2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. ( ZZ>= ` n ) )
65 fvexd 
 |-  ( ( ( 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 )
66 44 59 60 5 61 51 64 65 liminfequzmpt2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( liminf ` ( m e. ( ZZ>= ` n ) |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
67 44 59 60 5 61 51 64 53 liminfequzmpt2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( liminf ` ( m e. Z |-> B ) ) = ( liminf ` ( m e. ( ZZ>= ` n ) |-> B ) ) )
68 58 66 67 3eqtr4d 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( liminf ` ( m e. Z |-> B ) ) )
69 68 3exp 
 |-  ( ph -> ( n e. Z -> ( x e. |^|_ m e. ( ZZ>= ` n ) A -> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( liminf ` ( m e. Z |-> B ) ) ) ) )
70 3 40 69 rexlimd 
 |-  ( ph -> ( E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A -> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( liminf ` ( m e. Z |-> B ) ) ) )
71 70 adantr 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> ( E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A -> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( liminf ` ( m e. Z |-> B ) ) ) )
72 39 71 mpd 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( liminf ` ( m e. Z |-> B ) ) )
73 72 adantrr 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( liminf ` ( m e. Z |-> B ) ) e. RR ) ) -> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( liminf ` ( m e. Z |-> B ) ) )
74 simprr 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( liminf ` ( m e. Z |-> B ) ) e. RR ) ) -> ( liminf ` ( m e. Z |-> B ) ) e. RR )
75 73 74 eqeltrd 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( liminf ` ( m e. Z |-> B ) ) e. RR ) ) -> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR )
76 36 75 jca 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( liminf ` ( 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 ) /\ ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) )
77 simpl 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) /\ ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) ) -> ph )
78 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 ) )
79 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 )
80 79 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 )
81 78 80 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 )
82 81 adantrr 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) /\ ( liminf ` ( 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 )
83 simprr 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) /\ ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) ) -> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR )
84 simp2 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( liminf ` ( 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 72 eqcomd 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> ( liminf ` ( m e. Z |-> B ) ) = ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
86 85 3adant3 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) -> ( liminf ` ( m e. Z |-> B ) ) = ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
87 simp3 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) -> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR )
88 86 87 eqeltrd 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) -> ( liminf ` ( m e. Z |-> B ) ) e. RR )
89 84 88 jca 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( liminf ` ( 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 /\ ( liminf ` ( m e. Z |-> B ) ) e. RR ) )
90 77 82 83 89 syl3anc 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) /\ ( liminf ` ( 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 /\ ( liminf ` ( m e. Z |-> B ) ) e. RR ) )
91 76 90 impbida 
 |-  ( ph -> ( ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( liminf ` ( 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 ) /\ ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR ) ) )
92 2 91 rabbida3 
 |-  ( ph -> { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( liminf ` ( 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 ) | ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } )
93 12 92 eqtrd 
 |-  ( ph -> D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } )
94 9 eleq2i 
 |-  ( x e. D <-> x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( liminf ` ( m e. Z |-> B ) ) e. RR } )
95 94 biimpi 
 |-  ( x e. D -> x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( liminf ` ( m e. Z |-> B ) ) e. RR } )
96 rabidim1 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( liminf ` ( m e. Z |-> B ) ) e. RR } -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
97 95 96 syl 
 |-  ( x e. D -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
98 97 85 sylan2 
 |-  ( ( ph /\ x e. D ) -> ( liminf ` ( m e. Z |-> B ) ) = ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
99 2 93 98 mpteq12da 
 |-  ( ph -> ( x e. D |-> ( liminf ` ( 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 ) | ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } |-> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) ) )
100 11 99 eqtrd 
 |-  ( ph -> G = ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } |-> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) ) )
101 nfmpt1 
 |-  F/_ m ( m e. Z |-> ( x e. A |-> B ) )
102 nfcv 
 |-  F/_ x Z
103 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
104 102 103 nfmpt 
 |-  F/_ x ( m e. Z |-> ( x e. A |-> B ) )
105 1 8 fmptd2f 
 |-  ( ph -> ( m e. Z |-> ( x e. A |-> B ) ) : Z --> ( SMblFn ` S ) )
106 eqid 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( liminf ` ( 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 ) | ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR }
107 eqid 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } |-> ( liminf ` ( 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 ) | ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } |-> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
108 101 104 4 5 6 105 106 107 smfliminf 
 |-  ( ph -> ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) e. RR } |-> ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) ) e. ( SMblFn ` S ) )
109 100 108 eqeltrd 
 |-  ( ph -> G e. ( SMblFn ` S ) )