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 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 ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( liminf ` ( 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 simp2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. Z )
51 50 17 sylan 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
52 49 51 48 7 syl3anc 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> B e. V )
53 27 fvmpt2 
 |-  ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B )
54 48 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 46 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 43 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 ) -> ( liminf ` ( m e. ( ZZ>= ` n ) |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) = ( liminf ` ( m e. ( ZZ>= ` n ) |-> B ) ) )
58 nfcv 
 |-  F/_ m Z
59 nfcv 
 |-  F/_ m ( ZZ>= ` n )
60 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
61 5 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
62 61 uzidd 
 |-  ( n e. Z -> n e. ( ZZ>= ` n ) )
63 62 3ad2ant2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. ( ZZ>= ` n ) )
64 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 )
65 43 58 59 5 60 50 63 64 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 ) ) ) )
66 43 58 59 5 60 50 63 52 liminfequzmpt2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( liminf ` ( m e. Z |-> B ) ) = ( liminf ` ( m e. ( ZZ>= ` n ) |-> B ) ) )
67 57 65 66 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 ) ) )
68 67 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 ) ) ) ) )
69 3 39 68 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 ) ) ) )
70 69 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 ) ) ) )
71 38 70 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 ) ) )
72 71 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 ) ) )
73 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 )
74 72 73 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 )
75 36 74 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 ) )
76 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 )
77 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 ) )
78 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 )
79 78 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 )
80 77 79 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 )
81 80 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 )
82 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 )
83 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 )
84 71 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 ) ) ) )
85 84 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 ) ) ) )
86 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 )
87 85 86 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 )
88 83 87 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 ) )
89 76 81 82 88 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 ) )
90 75 89 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 ) ) )
91 2 90 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 } )
92 12 91 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 } )
93 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 } )
94 93 biimpi 
 |-  ( x e. D -> x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( liminf ` ( m e. Z |-> B ) ) e. RR } )
95 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 )
96 94 95 syl 
 |-  ( x e. D -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
97 96 84 sylan2 
 |-  ( ( ph /\ x e. D ) -> ( liminf ` ( m e. Z |-> B ) ) = ( liminf ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
98 2 92 97 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 ) ) ) ) )
99 11 98 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 ) ) ) ) )
100 nfmpt1 
 |-  F/_ m ( m e. Z |-> ( x e. A |-> B ) )
101 nfcv 
 |-  F/_ x Z
102 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
103 101 102 nfmpt 
 |-  F/_ x ( m e. Z |-> ( x e. A |-> B ) )
104 1 8 fmptd2f 
 |-  ( ph -> ( m e. Z |-> ( x e. A |-> B ) ) : Z --> ( SMblFn ` S ) )
105 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 }
106 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 ) ) ) )
107 100 103 4 5 6 104 105 106 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 ) )
108 99 107 eqeltrd 
 |-  ( ph -> G e. ( SMblFn ` S ) )