Metamath Proof Explorer

Theorem smflimmpt

Description: The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of Fremlin1 p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of Fremlin1 p. 39 ). A can contain m as a free variable, in other words it can be thought as an indexed collection A ( m ) . B can be thought as a collection with two indices B ( m , x ) . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 smflimmpt.p 
 |-  F/ m ph
2 smflimmpt.x 
 |-  F/ x ph
3 smflimmpt.n 
 |-  F/ n ph
4 smflimmpt.m 
 |-  ( ph -> M e. ZZ )
5 smflimmpt.z 
 |-  Z = ( ZZ>= ` M )
6 smflimmpt.a 
 |-  ( ( ph /\ m e. Z ) -> A e. V )
7 smflimmpt.b 
 |-  ( ( ph /\ m e. Z /\ x e. A ) -> B e. W )
8 smflimmpt.s 
 |-  ( ph -> S e. SAlg )
9 smflimmpt.l 
 |-  ( ( ph /\ m e. Z ) -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
10 smflimmpt.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( m e. Z |-> B ) e. dom ~~> }
11 smflimmpt.g 
 |-  G = ( x e. D |-> ( ~~> ` ( m e. Z |-> B ) ) )
12 11 a1i 
 |-  ( ph -> G = ( x e. D |-> ( ~~> ` ( m e. Z |-> B ) ) ) )
13 10 a1i 
 |-  ( ph -> D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( m e. Z |-> B ) e. dom ~~> } )
14 nfv 
 |-  F/ m n e. Z
15 1 14 nfan 
 |-  F/ m ( ph /\ n e. Z )
16 5 uztrn2 
 |-  ( ( n e. Z /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
17 16 adantll 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
18 simpll 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ph )
19 6 mptexd 
 |-  ( ( ph /\ m e. Z ) -> ( x e. A |-> B ) e. _V )
20 18 17 19 syl2anc 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( 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 17 20 22 syl2anc 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) = ( x e. A |-> B ) )
24 23 dmeqd 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) = dom ( x e. A |-> B ) )
25 nfv 
 |-  F/ x n e. Z
26 2 25 nfan 
 |-  F/ x ( ph /\ n e. Z )
27 nfv 
 |-  F/ x m e. ( ZZ>= ` n )
28 26 27 nfan 
 |-  F/ x ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) )
29 simplll 
 |-  ( ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) /\ x e. A ) -> ph )
30 17 adantr 
 |-  ( ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) /\ x e. A ) -> m e. Z )
31 simpr 
 |-  ( ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) /\ x e. A ) -> x e. A )
32 29 30 31 7 syl3anc 
 |-  ( ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) /\ x e. A ) -> B e. W )
33 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
34 28 32 33 fnmptd 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( x e. A |-> B ) Fn A )
35 34 fndmd 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> dom ( x e. A |-> B ) = A )
36 24 35 eqtr2d 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> A = dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
37 15 36 iineq2d 
 |-  ( ( ph /\ n e. Z ) -> |^|_ m e. ( ZZ>= ` n ) A = |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
38 3 37 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 ) )
39 simpr 
 |-  ( ( ph /\ m e. Z ) -> m e. Z )
40 39 19 22 syl2anc 
 |-  ( ( ph /\ m e. Z ) -> ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) = ( x e. A |-> B ) )
41 40 eqcomd 
 |-  ( ( ph /\ m e. Z ) -> ( x e. A |-> B ) = ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
42 41 dmeqd 
 |-  ( ( ph /\ m e. Z ) -> dom ( x e. A |-> B ) = dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
43 18 17 42 syl2anc 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> dom ( x e. A |-> B ) = dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
44 15 43 iineq2d 
 |-  ( ( ph /\ n e. Z ) -> |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) = |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
45 3 44 iuneq2df 
 |-  ( ph -> U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) )
46 38 45 eqtr4d 
 |-  ( ph -> U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) )
47 46 eleq2d 
 |-  ( ph -> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A <-> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) ) )
48 47 biimpa 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) )
49 48 adantrr 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( m e. Z |-> B ) e. dom ~~> ) ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) )
50 eliun 
 |-  ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A <-> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A )
51 50 biimpi 
 |-  ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A )
52 51 adantl 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A ) -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A )
53 52 adantrr 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( m e. Z |-> B ) e. dom ~~> ) ) -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A )
54 nfv 
 |-  F/ n ( m e. Z |-> B ) e. dom ~~>
55 3 54 nfan 
 |-  F/ n ( ph /\ ( m e. Z |-> B ) e. dom ~~> )
56 nfv 
 |-  F/ n ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~>
57 simpllr 
 |-  ( ( ( ( ph /\ ( m e. Z |-> B ) e. dom ~~> ) /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( m e. Z |-> B ) e. dom ~~> )
58 nfcv 
 |-  F/_ m x
59 nfii1 
 |-  F/_ m |^|_ m e. ( ZZ>= ` n ) A
60 58 59 nfel 
 |-  F/ m x e. |^|_ m e. ( ZZ>= ` n ) A
61 15 60 nfan 
 |-  F/ m ( ( ph /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A )
62 5 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
63 62 ad2antlr 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. ZZ )
64 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
65 5 fvexi 
 |-  Z e. _V
66 65 a1i 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> Z e. _V )
67 5 uzssd3 
 |-  ( n e. Z -> ( ZZ>= ` n ) C_ Z )
68 67 ad2antlr 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( ZZ>= ` n ) C_ Z )
69 fvexd 
 |-  ( ( ( ( ph /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ( ( x e. A |-> B ) ` x ) e. _V )
70 eliinid 
 |-  ( ( x e. |^|_ m e. ( ZZ>= ` n ) A /\ m e. ( ZZ>= ` n ) ) -> x e. A )
71 70 adantll 
 |-  ( ( ( ( ph /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> x e. A )
72 18 adantlr 
 |-  ( ( ( ( ph /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ph )
73 17 adantlr 
 |-  ( ( ( ( ph /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
74 72 73 71 7 syl3anc 
 |-  ( ( ( ( ph /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> B e. W )
75 33 fvmpt2 
 |-  ( ( x e. A /\ B e. W ) -> ( ( x e. A |-> B ) ` x ) = B )
76 71 74 75 syl2anc 
 |-  ( ( ( ( ph /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ( ( x e. A |-> B ) ` x ) = B )
77 61 63 64 66 66 68 68 69 76 climeldmeqmpt3 
 |-  ( ( ( ph /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> <-> ( m e. Z |-> B ) e. dom ~~> ) )
78 77 adantllr 
 |-  ( ( ( ( ph /\ ( m e. Z |-> B ) e. dom ~~> ) /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> <-> ( m e. Z |-> B ) e. dom ~~> ) )
79 57 78 mpbird 
 |-  ( ( ( ( ph /\ ( m e. Z |-> B ) e. dom ~~> ) /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> )
80 79 exp31 
 |-  ( ( ph /\ ( m e. Z |-> B ) e. dom ~~> ) -> ( n e. Z -> ( x e. |^|_ m e. ( ZZ>= ` n ) A -> ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) ) )
81 55 56 80 rexlimd 
 |-  ( ( ph /\ ( m e. Z |-> B ) e. dom ~~> ) -> ( E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A -> ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) )
82 81 adantrl 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( m e. Z |-> B ) e. dom ~~> ) ) -> ( E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A -> ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) )
83 53 82 mpd 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( m e. Z |-> B ) e. dom ~~> ) ) -> ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> )
84 49 83 jca 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( m e. Z |-> B ) e. dom ~~> ) ) -> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) )
85 84 ex 
 |-  ( ph -> ( ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( m e. Z |-> B ) e. dom ~~> ) -> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) ) )
86 47 biimpar 
 |-  ( ( ph /\ x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
87 86 adantrr 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
88 87 51 syl 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) ) -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A )
89 3 56 nfan 
 |-  F/ n ( ph /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> )
90 simpllr 
 |-  ( ( ( ( ph /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> )
91 77 adantllr 
 |-  ( ( ( ( ph /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> <-> ( m e. Z |-> B ) e. dom ~~> ) )
92 90 91 mpbid 
 |-  ( ( ( ( ph /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) /\ n e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( m e. Z |-> B ) e. dom ~~> )
93 92 exp31 
 |-  ( ( ph /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) -> ( n e. Z -> ( x e. |^|_ m e. ( ZZ>= ` n ) A -> ( m e. Z |-> B ) e. dom ~~> ) ) )
94 89 54 93 rexlimd 
 |-  ( ( ph /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) -> ( E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A -> ( m e. Z |-> B ) e. dom ~~> ) )
95 94 adantrl 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) ) -> ( E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A -> ( m e. Z |-> B ) e. dom ~~> ) )
96 88 95 mpd 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) ) -> ( m e. Z |-> B ) e. dom ~~> )
97 87 96 jca 
 |-  ( ( ph /\ ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) ) -> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( m e. Z |-> B ) e. dom ~~> ) )
98 97 ex 
 |-  ( ph -> ( ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) -> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( m e. Z |-> B ) e. dom ~~> ) ) )
99 85 98 impbid 
 |-  ( ph -> ( ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A /\ ( m e. Z |-> B ) e. dom ~~> ) <-> ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) /\ ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> ) ) )
100 2 99 rabbida3 
 |-  ( ph -> { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( m e. Z |-> B ) e. dom ~~> } = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) | ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> } )
101 13 100 eqtrd 
 |-  ( ph -> D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) | ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> } )
102 10 eleq2i 
 |-  ( x e. D <-> x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( m e. Z |-> B ) e. dom ~~> } )
103 102 biimpi 
 |-  ( x e. D -> x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( m e. Z |-> B ) e. dom ~~> } )
104 rabidim1 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( m e. Z |-> B ) e. dom ~~> } -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A )
105 103 104 51 3syl 
 |-  ( x e. D -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A )
106 105 adantl 
 |-  ( ( ph /\ x e. D ) -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A )
107 nfcv 
 |-  F/_ n x
108 nfiu1 
 |-  F/_ n U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A
109 54 108 nfrabw 
 |-  F/_ n { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) A | ( m e. Z |-> B ) e. dom ~~> }
110 10 109 nfcxfr 
 |-  F/_ n D
111 107 110 nfel 
 |-  F/ n x e. D
112 3 111 nfan 
 |-  F/ n ( ph /\ x e. D )
113 nfv 
 |-  F/ n ( ~~> ` ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) ) = ( ~~> ` ( m e. Z |-> B ) )
114 1 14 60 nf3an 
 |-  F/ m ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A )
115 simp2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. Z )
116 115 62 syl 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> n e. ZZ )
117 65 a1i 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> Z e. _V )
118 5 115 uzssd2 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( ZZ>= ` n ) C_ Z )
119 fvexd 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ( ( x e. A |-> B ) ` x ) e. _V )
120 70 3ad2antl3 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> x e. A )
121 simpl1 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ph )
122 115 16 sylan 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
123 121 122 120 7 syl3anc 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> B e. W )
124 120 123 75 syl2anc 
 |-  ( ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) /\ m e. ( ZZ>= ` n ) ) -> ( ( x e. A |-> B ) ` x ) = B )
125 114 116 64 117 117 118 118 119 124 climfveqmpt3 
 |-  ( ( ph /\ n e. Z /\ x e. |^|_ m e. ( ZZ>= ` n ) A ) -> ( ~~> ` ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) ) = ( ~~> ` ( m e. Z |-> B ) ) )
126 125 3exp 
 |-  ( ph -> ( n e. Z -> ( x e. |^|_ m e. ( ZZ>= ` n ) A -> ( ~~> ` ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) ) = ( ~~> ` ( m e. Z |-> B ) ) ) ) )
127 126 adantr 
 |-  ( ( ph /\ x e. D ) -> ( n e. Z -> ( x e. |^|_ m e. ( ZZ>= ` n ) A -> ( ~~> ` ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) ) = ( ~~> ` ( m e. Z |-> B ) ) ) ) )
128 112 113 127 rexlimd 
 |-  ( ( ph /\ x e. D ) -> ( E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) A -> ( ~~> ` ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) ) = ( ~~> ` ( m e. Z |-> B ) ) ) )
129 106 128 mpd 
 |-  ( ( ph /\ x e. D ) -> ( ~~> ` ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) ) = ( ~~> ` ( m e. Z |-> B ) ) )
130 129 eqcomd 
 |-  ( ( ph /\ x e. D ) -> ( ~~> ` ( m e. Z |-> B ) ) = ( ~~> ` ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) ) )
131 2 101 130 mpteq12da 
 |-  ( ph -> ( x e. D |-> ( ~~> ` ( m e. Z |-> B ) ) ) = ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) | ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) ) ) )
132 41 eqcomd 
 |-  ( ( ph /\ m e. Z ) -> ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) = ( x e. A |-> B ) )
133 132 fveq1d 
 |-  ( ( ph /\ m e. Z ) -> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) = ( ( x e. A |-> B ) ` x ) )
134 1 133 mpteq2da 
 |-  ( ph -> ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) = ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) )
135 134 eqcomd 
 |-  ( ph -> ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) = ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) )
136 135 eleq1d 
 |-  ( ph -> ( ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> <-> ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) e. dom ~~> ) )
137 2 45 136 rabbida2 
 |-  ( ph -> { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) | ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> } = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) e. dom ~~> } )
138 133 eqcomd 
 |-  ( ( ph /\ m e. Z ) -> ( ( x e. A |-> B ) ` x ) = ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) )
139 1 138 mpteq2da 
 |-  ( ph -> ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) = ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) )
140 139 fveq2d 
 |-  ( ph -> ( ~~> ` ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) ) = ( ~~> ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
141 2 137 140 mpteq12df 
 |-  ( ph -> ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( x e. A |-> B ) | ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( m e. Z |-> ( ( x e. A |-> B ) ` x ) ) ) ) = ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) ) )
142 12 131 141 3eqtrd 
 |-  ( ph -> G = ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) ) )
143 nfmpt1 
 |-  F/_ m ( m e. Z |-> ( x e. A |-> B ) )
144 nfcv 
 |-  F/_ x Z
145 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
146 144 145 nfmpt 
 |-  F/_ x ( m e. Z |-> ( x e. A |-> B ) )
147 1 9 21 fmptdf 
 |-  ( ph -> ( m e. Z |-> ( x e. A |-> B ) ) : Z --> ( SMblFn ` S ) )
148 eqid 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) e. dom ~~> } = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) e. dom ~~> }
149 eqid 
 |-  ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( 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 ) | ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) )
150 143 146 4 5 8 147 148 149 smflim2 
 |-  ( ph -> ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) | ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) e. dom ~~> } |-> ( ~~> ` ( m e. Z |-> ( ( ( m e. Z |-> ( x e. A |-> B ) ) ` m ) ` x ) ) ) ) e. ( SMblFn ` S ) )
151 142 150 eqeltrd 
 |-  ( ph -> G e. ( SMblFn ` S ) )