Metamath Proof Explorer

Theorem smflim

Description: The limit 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 ). (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smflim.n 
|- F/_ m F
smflim.x 
|- F/_ x F
smflim.m 
|- ( ph -> M e. ZZ )
smflim.z 
|- Z = ( ZZ>= ` M )
smflim.s 
|- ( ph -> S e. SAlg )
smflim.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smflim.d 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
smflim.g 
|- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
Assertion smflim 
|- ( ph -> G e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smflim.n 
 |-  F/_ m F
2 smflim.x 
 |-  F/_ x F
3 smflim.m 
 |-  ( ph -> M e. ZZ )
4 smflim.z 
 |-  Z = ( ZZ>= ` M )
5 smflim.s 
 |-  ( ph -> S e. SAlg )
6 smflim.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
7 smflim.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
8 smflim.g 
 |-  G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
9 nfv 
 |-  F/ a ph
10 nfcv 
 |-  F/_ x Z
11 nfcv 
 |-  F/_ x ( ZZ>= ` n )
12 nfcv 
 |-  F/_ x m
13 2 12 nffv 
 |-  F/_ x ( F ` m )
14 13 nfdm 
 |-  F/_ x dom ( F ` m )
15 11 14 nfiin 
 |-  F/_ x |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
16 10 15 nfiun 
 |-  F/_ x U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
17 16 ssrab2f 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
18 7 17 eqsstri 
 |-  D C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
19 18 a1i 
 |-  ( ph -> D C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
20 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
21 4 eleq2i 
 |-  ( n e. Z <-> n e. ( ZZ>= ` M ) )
22 21 biimpi 
 |-  ( n e. Z -> n e. ( ZZ>= ` M ) )
23 20 22 sselid 
 |-  ( n e. Z -> n e. ZZ )
24 uzid 
 |-  ( n e. ZZ -> n e. ( ZZ>= ` n ) )
25 23 24 syl 
 |-  ( n e. Z -> n e. ( ZZ>= ` n ) )
26 25 adantl 
 |-  ( ( ph /\ n e. Z ) -> n e. ( ZZ>= ` n ) )
27 5 adantr 
 |-  ( ( ph /\ n e. Z ) -> S e. SAlg )
28 6 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. ( SMblFn ` S ) )
29 eqid 
 |-  dom ( F ` n ) = dom ( F ` n )
30 27 28 29 smfdmss 
 |-  ( ( ph /\ n e. Z ) -> dom ( F ` n ) C_ U. S )
31 nfcv 
 |-  F/_ m n
32 1 31 nffv 
 |-  F/_ m ( F ` n )
33 32 nfdm 
 |-  F/_ m dom ( F ` n )
34 nfcv 
 |-  F/_ m U. S
35 33 34 nfss 
 |-  F/ m dom ( F ` n ) C_ U. S
36 fveq2 
 |-  ( m = n -> ( F ` m ) = ( F ` n ) )
37 36 dmeqd 
 |-  ( m = n -> dom ( F ` m ) = dom ( F ` n ) )
38 37 sseq1d 
 |-  ( m = n -> ( dom ( F ` m ) C_ U. S <-> dom ( F ` n ) C_ U. S ) )
39 35 38 rspce 
 |-  ( ( n e. ( ZZ>= ` n ) /\ dom ( F ` n ) C_ U. S ) -> E. m e. ( ZZ>= ` n ) dom ( F ` m ) C_ U. S )
40 26 30 39 syl2anc 
 |-  ( ( ph /\ n e. Z ) -> E. m e. ( ZZ>= ` n ) dom ( F ` m ) C_ U. S )
41 iinss 
 |-  ( E. m e. ( ZZ>= ` n ) dom ( F ` m ) C_ U. S -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) C_ U. S )
42 40 41 syl 
 |-  ( ( ph /\ n e. Z ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) C_ U. S )
43 42 iunssd 
 |-  ( ph -> U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) C_ U. S )
44 19 43 sstrd 
 |-  ( ph -> D C_ U. S )
45 nfv 
 |-  F/ m ph
46 nfcv 
 |-  F/_ m y
47 nfmpt1 
 |-  F/_ m ( m e. Z |-> ( ( F ` m ) ` x ) )
48 nfcv 
 |-  F/_ m dom ~~>
49 47 48 nfel 
 |-  F/ m ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~>
50 nfcv 
 |-  F/_ m Z
51 nfii1 
 |-  F/_ m |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
52 50 51 nfiun 
 |-  F/_ m U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
53 49 52 nfrabw 
 |-  F/_ m { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
54 7 53 nfcxfr 
 |-  F/_ m D
55 46 54 nfel 
 |-  F/ m y e. D
56 45 55 nfan 
 |-  F/ m ( ph /\ y e. D )
57 nfcv 
 |-  F/_ w F
58 5 adantr 
 |-  ( ( ph /\ m e. Z ) -> S e. SAlg )
59 6 ffvelrnda 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
60 eqid 
 |-  dom ( F ` m ) = dom ( F ` m )
61 58 59 60 smff 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
62 61 adantlr 
 |-  ( ( ( ph /\ y e. D ) /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
63 nfcv 
 |-  F/_ y U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
64 nfv 
 |-  F/ y ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~>
65 nfcv 
 |-  F/_ x y
66 13 65 nffv 
 |-  F/_ x ( ( F ` m ) ` y )
67 10 66 nfmpt 
 |-  F/_ x ( m e. Z |-> ( ( F ` m ) ` y ) )
68 67 nfel1 
 |-  F/ x ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~>
69 fveq2 
 |-  ( x = y -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` y ) )
70 69 mpteq2dv 
 |-  ( x = y -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` y ) ) )
71 70 eleq1d 
 |-  ( x = y -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> <-> ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~> ) )
72 16 63 64 68 71 cbvrabw 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } = { y e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~> }
73 nfcv 
 |-  F/_ l dom ( F ` m )
74 nfcv 
 |-  F/_ m l
75 1 74 nffv 
 |-  F/_ m ( F ` l )
76 75 nfdm 
 |-  F/_ m dom ( F ` l )
77 fveq2 
 |-  ( m = l -> ( F ` m ) = ( F ` l ) )
78 77 dmeqd 
 |-  ( m = l -> dom ( F ` m ) = dom ( F ` l ) )
79 73 76 78 cbviin 
 |-  |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ l e. ( ZZ>= ` n ) dom ( F ` l )
80 79 a1i 
 |-  ( n = i -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ l e. ( ZZ>= ` n ) dom ( F ` l ) )
81 fveq2 
 |-  ( n = i -> ( ZZ>= ` n ) = ( ZZ>= ` i ) )
82 eqidd 
 |-  ( ( n = i /\ l e. ( ZZ>= ` i ) ) -> dom ( F ` l ) = dom ( F ` l ) )
83 81 82 iineq12dv 
 |-  ( n = i -> |^|_ l e. ( ZZ>= ` n ) dom ( F ` l ) = |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) )
84 80 83 eqtrd 
 |-  ( n = i -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) )
85 84 cbviunv 
 |-  U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ i e. Z |^|_ l e. ( ZZ>= ` i ) dom ( F ` l )
86 85 eleq2i 
 |-  ( y e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> y e. U_ i e. Z |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) )
87 nfcv 
 |-  F/_ l Z
88 nfcv 
 |-  F/_ l ( ( F ` m ) ` y )
89 75 46 nffv 
 |-  F/_ m ( ( F ` l ) ` y )
90 77 fveq1d 
 |-  ( m = l -> ( ( F ` m ) ` y ) = ( ( F ` l ) ` y ) )
91 50 87 88 89 90 cbvmptf 
 |-  ( m e. Z |-> ( ( F ` m ) ` y ) ) = ( l e. Z |-> ( ( F ` l ) ` y ) )
92 91 eleq1i 
 |-  ( ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~> <-> ( l e. Z |-> ( ( F ` l ) ` y ) ) e. dom ~~> )
93 86 92 anbi12i 
 |-  ( ( y e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~> ) <-> ( y e. U_ i e. Z |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) /\ ( l e. Z |-> ( ( F ` l ) ` y ) ) e. dom ~~> ) )
94 93 rabbia2 
 |-  { y e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~> } = { y e. U_ i e. Z |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) | ( l e. Z |-> ( ( F ` l ) ` y ) ) e. dom ~~> }
95 7 72 94 3eqtri 
 |-  D = { y e. U_ i e. Z |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) | ( l e. Z |-> ( ( F ` l ) ` y ) ) e. dom ~~> }
96 fveq2 
 |-  ( y = w -> ( ( F ` l ) ` y ) = ( ( F ` l ) ` w ) )
97 96 mpteq2dv 
 |-  ( y = w -> ( l e. Z |-> ( ( F ` l ) ` y ) ) = ( l e. Z |-> ( ( F ` l ) ` w ) ) )
98 97 eleq1d 
 |-  ( y = w -> ( ( l e. Z |-> ( ( F ` l ) ` y ) ) e. dom ~~> <-> ( l e. Z |-> ( ( F ` l ) ` w ) ) e. dom ~~> ) )
99 98 cbvrabv 
 |-  { y e. U_ i e. Z |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) | ( l e. Z |-> ( ( F ` l ) ` y ) ) e. dom ~~> } = { w e. U_ i e. Z |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) | ( l e. Z |-> ( ( F ` l ) ` w ) ) e. dom ~~> }
100 fveq2 
 |-  ( l = m -> ( F ` l ) = ( F ` m ) )
101 100 dmeqd 
 |-  ( l = m -> dom ( F ` l ) = dom ( F ` m ) )
102 76 73 101 cbviin 
 |-  |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) = |^|_ m e. ( ZZ>= ` i ) dom ( F ` m )
103 102 a1i 
 |-  ( i e. Z -> |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) = |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
104 103 iuneq2i 
 |-  U_ i e. Z |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) = U_ i e. Z |^|_ m e. ( ZZ>= ` i ) dom ( F ` m )
105 104 eleq2i 
 |-  ( w e. U_ i e. Z |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) <-> w e. U_ i e. Z |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
106 nfcv 
 |-  F/_ m w
107 75 106 nffv 
 |-  F/_ m ( ( F ` l ) ` w )
108 nfcv 
 |-  F/_ l ( ( F ` m ) ` w )
109 100 fveq1d 
 |-  ( l = m -> ( ( F ` l ) ` w ) = ( ( F ` m ) ` w ) )
110 87 50 107 108 109 cbvmptf 
 |-  ( l e. Z |-> ( ( F ` l ) ` w ) ) = ( m e. Z |-> ( ( F ` m ) ` w ) )
111 110 eleq1i 
 |-  ( ( l e. Z |-> ( ( F ` l ) ` w ) ) e. dom ~~> <-> ( m e. Z |-> ( ( F ` m ) ` w ) ) e. dom ~~> )
112 105 111 anbi12i 
 |-  ( ( w e. U_ i e. Z |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) /\ ( l e. Z |-> ( ( F ` l ) ` w ) ) e. dom ~~> ) <-> ( w e. U_ i e. Z |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) /\ ( m e. Z |-> ( ( F ` m ) ` w ) ) e. dom ~~> ) )
113 112 rabbia2 
 |-  { w e. U_ i e. Z |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) | ( l e. Z |-> ( ( F ` l ) ` w ) ) e. dom ~~> } = { w e. U_ i e. Z |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` w ) ) e. dom ~~> }
114 99 113 eqtri 
 |-  { y e. U_ i e. Z |^|_ l e. ( ZZ>= ` i ) dom ( F ` l ) | ( l e. Z |-> ( ( F ` l ) ` y ) ) e. dom ~~> } = { w e. U_ i e. Z |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` w ) ) e. dom ~~> }
115 95 114 eqtri 
 |-  D = { w e. U_ i e. Z |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` w ) ) e. dom ~~> }
116 simpr 
 |-  ( ( ph /\ y e. D ) -> y e. D )
117 56 1 57 4 62 115 116 fnlimfvre 
 |-  ( ( ph /\ y e. D ) -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` y ) ) ) e. RR )
118 nfrab1 
 |-  F/_ x { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
119 7 118 nfcxfr 
 |-  F/_ x D
120 nfcv 
 |-  F/_ y D
121 nfcv 
 |-  F/_ y ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) )
122 nfcv 
 |-  F/_ x ~~>
123 122 67 nffv 
 |-  F/_ x ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` y ) ) )
124 70 fveq2d 
 |-  ( x = y -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` y ) ) ) )
125 119 120 121 123 124 cbvmptf 
 |-  ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) = ( y e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` y ) ) ) )
126 8 125 eqtri 
 |-  G = ( y e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` y ) ) ) )
127 117 126 fmptd 
 |-  ( ph -> G : D --> RR )
128 3 adantr 
 |-  ( ( ph /\ a e. RR ) -> M e. ZZ )
129 5 adantr 
 |-  ( ( ph /\ a e. RR ) -> S e. SAlg )
130 6 adantr 
 |-  ( ( ph /\ a e. RR ) -> F : Z --> ( SMblFn ` S ) )
131 nfcv 
 |-  F/_ x l
132 2 131 nffv 
 |-  F/_ x ( F ` l )
133 132 65 nffv 
 |-  F/_ x ( ( F ` l ) ` y )
134 10 133 nfmpt 
 |-  F/_ x ( l e. Z |-> ( ( F ` l ) ` y ) )
135 122 134 nffv 
 |-  F/_ x ( ~~> ` ( l e. Z |-> ( ( F ` l ) ` y ) ) )
136 nfcv 
 |-  F/_ l ( ( F ` m ) ` x )
137 nfcv 
 |-  F/_ m x
138 75 137 nffv 
 |-  F/_ m ( ( F ` l ) ` x )
139 77 fveq1d 
 |-  ( m = l -> ( ( F ` m ) ` x ) = ( ( F ` l ) ` x ) )
140 50 87 136 138 139 cbvmptf 
 |-  ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( l e. Z |-> ( ( F ` l ) ` x ) )
141 140 a1i 
 |-  ( x = y -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( l e. Z |-> ( ( F ` l ) ` x ) ) )
142 simpl 
 |-  ( ( x = y /\ l e. Z ) -> x = y )
143 142 fveq2d 
 |-  ( ( x = y /\ l e. Z ) -> ( ( F ` l ) ` x ) = ( ( F ` l ) ` y ) )
144 143 mpteq2dva 
 |-  ( x = y -> ( l e. Z |-> ( ( F ` l ) ` x ) ) = ( l e. Z |-> ( ( F ` l ) ` y ) ) )
145 141 144 eqtrd 
 |-  ( x = y -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( l e. Z |-> ( ( F ` l ) ` y ) ) )
146 145 fveq2d 
 |-  ( x = y -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( ~~> ` ( l e. Z |-> ( ( F ` l ) ` y ) ) ) )
147 119 120 121 135 146 cbvmptf 
 |-  ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) = ( y e. D |-> ( ~~> ` ( l e. Z |-> ( ( F ` l ) ` y ) ) ) )
148 8 147 eqtri 
 |-  G = ( y e. D |-> ( ~~> ` ( l e. Z |-> ( ( F ` l ) ` y ) ) ) )
149 simpr 
 |-  ( ( ph /\ a e. RR ) -> a e. RR )
150 nfcv 
 |-  F/_ m <
151 nfcv 
 |-  F/_ m ( a + ( 1 / j ) )
152 89 150 151 nfbr 
 |-  F/ m ( ( F ` l ) ` y ) < ( a + ( 1 / j ) )
153 152 76 nfrabw 
 |-  F/_ m { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) }
154 nfcv 
 |-  F/_ m t
155 154 76 nfin 
 |-  F/_ m ( t i^i dom ( F ` l ) )
156 153 155 nfeq 
 |-  F/ m { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) } = ( t i^i dom ( F ` l ) )
157 nfcv 
 |-  F/_ m S
158 156 157 nfrabw 
 |-  F/_ m { t e. S | { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) } = ( t i^i dom ( F ` l ) ) }
159 nfcv 
 |-  F/_ k { t e. S | { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) } = ( t i^i dom ( F ` l ) ) }
160 nfcv 
 |-  F/_ l { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) }
161 nfcv 
 |-  F/_ j { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) }
162 nfcv 
 |-  F/_ y dom ( F ` l )
163 132 nfdm 
 |-  F/_ x dom ( F ` l )
164 nfcv 
 |-  F/_ x <
165 nfcv 
 |-  F/_ x ( a + ( 1 / j ) )
166 133 164 165 nfbr 
 |-  F/ x ( ( F ` l ) ` y ) < ( a + ( 1 / j ) )
167 nfv 
 |-  F/ y ( ( F ` l ) ` x ) < ( a + ( 1 / j ) )
168 fveq2 
 |-  ( y = x -> ( ( F ` l ) ` y ) = ( ( F ` l ) ` x ) )
169 168 breq1d 
 |-  ( y = x -> ( ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) <-> ( ( F ` l ) ` x ) < ( a + ( 1 / j ) ) ) )
170 162 163 166 167 169 cbvrabw 
 |-  { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) } = { x e. dom ( F ` l ) | ( ( F ` l ) ` x ) < ( a + ( 1 / j ) ) }
171 170 a1i 
 |-  ( t = s -> { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) } = { x e. dom ( F ` l ) | ( ( F ` l ) ` x ) < ( a + ( 1 / j ) ) } )
172 ineq1 
 |-  ( t = s -> ( t i^i dom ( F ` l ) ) = ( s i^i dom ( F ` l ) ) )
173 171 172 eqeq12d 
 |-  ( t = s -> ( { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) } = ( t i^i dom ( F ` l ) ) <-> { x e. dom ( F ` l ) | ( ( F ` l ) ` x ) < ( a + ( 1 / j ) ) } = ( s i^i dom ( F ` l ) ) ) )
174 173 cbvrabv 
 |-  { t e. S | { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) } = ( t i^i dom ( F ` l ) ) } = { s e. S | { x e. dom ( F ` l ) | ( ( F ` l ) ` x ) < ( a + ( 1 / j ) ) } = ( s i^i dom ( F ` l ) ) }
175 174 a1i 
 |-  ( l = m -> { t e. S | { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) } = ( t i^i dom ( F ` l ) ) } = { s e. S | { x e. dom ( F ` l ) | ( ( F ` l ) ` x ) < ( a + ( 1 / j ) ) } = ( s i^i dom ( F ` l ) ) } )
176 101 eleq2d 
 |-  ( l = m -> ( x e. dom ( F ` l ) <-> x e. dom ( F ` m ) ) )
177 100 fveq1d 
 |-  ( l = m -> ( ( F ` l ) ` x ) = ( ( F ` m ) ` x ) )
178 177 breq1d 
 |-  ( l = m -> ( ( ( F ` l ) ` x ) < ( a + ( 1 / j ) ) <-> ( ( F ` m ) ` x ) < ( a + ( 1 / j ) ) ) )
179 176 178 anbi12d 
 |-  ( l = m -> ( ( x e. dom ( F ` l ) /\ ( ( F ` l ) ` x ) < ( a + ( 1 / j ) ) ) <-> ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( a + ( 1 / j ) ) ) ) )
180 179 rabbidva2 
 |-  ( l = m -> { x e. dom ( F ` l ) | ( ( F ` l ) ` x ) < ( a + ( 1 / j ) ) } = { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / j ) ) } )
181 101 ineq2d 
 |-  ( l = m -> ( s i^i dom ( F ` l ) ) = ( s i^i dom ( F ` m ) ) )
182 180 181 eqeq12d 
 |-  ( l = m -> ( { x e. dom ( F ` l ) | ( ( F ` l ) ` x ) < ( a + ( 1 / j ) ) } = ( s i^i dom ( F ` l ) ) <-> { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / j ) ) } = ( s i^i dom ( F ` m ) ) ) )
183 182 rabbidv 
 |-  ( l = m -> { s e. S | { x e. dom ( F ` l ) | ( ( F ` l ) ` x ) < ( a + ( 1 / j ) ) } = ( s i^i dom ( F ` l ) ) } = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / j ) ) } = ( s i^i dom ( F ` m ) ) } )
184 175 183 eqtrd 
 |-  ( l = m -> { t e. S | { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) } = ( t i^i dom ( F ` l ) ) } = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / j ) ) } = ( s i^i dom ( F ` m ) ) } )
185 oveq2 
 |-  ( j = k -> ( 1 / j ) = ( 1 / k ) )
186 185 oveq2d 
 |-  ( j = k -> ( a + ( 1 / j ) ) = ( a + ( 1 / k ) ) )
187 186 breq2d 
 |-  ( j = k -> ( ( ( F ` m ) ` x ) < ( a + ( 1 / j ) ) <-> ( ( F ` m ) ` x ) < ( a + ( 1 / k ) ) ) )
188 187 rabbidv 
 |-  ( j = k -> { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / j ) ) } = { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / k ) ) } )
189 188 eqeq1d 
 |-  ( j = k -> ( { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / j ) ) } = ( s i^i dom ( F ` m ) ) <-> { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) ) )
190 189 rabbidv 
 |-  ( j = k -> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / j ) ) } = ( s i^i dom ( F ` m ) ) } = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
191 184 190 sylan9eq 
 |-  ( ( l = m /\ j = k ) -> { t e. S | { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) } = ( t i^i dom ( F ` l ) ) } = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
192 158 159 160 161 191 cbvmpo 
 |-  ( l e. Z , j e. NN |-> { t e. S | { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) } = ( t i^i dom ( F ` l ) ) } ) = ( m e. Z , k e. NN |-> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
193 192 eqcomi 
 |-  ( m e. Z , k e. NN |-> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( a + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } ) = ( l e. Z , j e. NN |-> { t e. S | { y e. dom ( F ` l ) | ( ( F ` l ) ` y ) < ( a + ( 1 / j ) ) } = ( t i^i dom ( F ` l ) ) } )
194 128 4 129 130 95 148 149 193 smflimlem6 
 |-  ( ( ph /\ a e. RR ) -> { y e. D | ( G ` y ) <_ a } e. ( S |`t D ) )
195 9 5 44 127 194 issmfled 
 |-  ( ph -> G e. ( SMblFn ` S ) )