Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smflimlem2 Structured version   Visualization version   Unicode version
Theorem smflimlem2 40980
Description: Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by D. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
smflimlem2.1 |- Z = ( ZZ>= ` M )
smflimlem2.2 |- ( ph -> S e. SAlg )
smflimlem2.3 |- ( ph -> F : Z --> (SMblFn ` S ) )
smflimlem2.4 |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
smflimlem2.5 |- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
smflimlem2.6 |- ( ph -> A e. RR )
smflimlem2.7 |- P = ( 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 ) ) } )
smflimlem2.8 |- H = ( m e. Z , k e. NN |-> ( C ` ( m P k ) ) )
smflimlem2.9 |- I = |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k )
smflimlem2.10 |- ( ( ph /\ r e. ran P ) -> ( C ` r ) e. r )
Assertion
Ref Expression
smflimlem2 |- ( ph -> { x e. D | ( G ` x ) <_ A } C_ ( D i^i I ) )
Distinct variable groups:   x, k   A, k, m, n   A, s, k, m   C, r   D, k, m, n   n, F, x   F, s, x   k, G, m, n   H, s   x, I   P, r   S, s   k, Z, m, n, x   ph, k, m, n, x   k, r, m, ph
Allowed substitution hints:   ph( s)   A( x, r)   C( x, k, m, n, s)   D( x, s, r)   P( x, k, m, n, s)   S( x, k, m, n, r)   F( k, m, r)   G( x, s, r)   H( x, k, m, n, r)   I( k, m, n, s, r)   M( x, k, m, n, s, r)   Z( s, r)
Proof of Theorem smflimlem2
Dummy variables i j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smflimlem2.4 . . . . 5 |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
2 nfrab1 3122 . . . . 5 |- F/_ x { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
31, 2nfcxfr 2762 . . . 4 |- F/_ x D
43ssrab2f 39300 . . 3 |- { x e. D | ( G ` x ) <_ A } C_ D
54a1i 11 . 2 |- ( ph -> { x e. D | ( G ` x ) <_ A } C_ D )
6 simpllr 799 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) -> x e. D )
7 ssrab2 3687 . . . . . . . . . . . . . . 15 |- { 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 )
81, 7eqsstri 3635 . . . . . . . . . . . . . 14 |- D C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
98sseli 3599 . . . . . . . . . . . . 13 |- ( x e. D -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
10 fveq2 6191 . . . . . . . . . . . . . . . . 17 |- ( n = i -> ( ZZ>= ` n ) = ( ZZ>= ` i ) )
1110iineq1d 39267 . . . . . . . . . . . . . . . 16 |- ( n = i -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
1211cbviunv 4559 . . . . . . . . . . . . . . 15 |- U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ i e. Z |^|_ m e. ( ZZ>= ` i ) dom ( F ` m )
1312eleq2i 2693 . . . . . . . . . . . . . 14 |- ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> x e. U_ i e. Z |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
14 eliun 4524 . . . . . . . . . . . . . 14 |- ( x e. U_ i e. Z |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) <-> E. i e. Z x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
1513, 14bitri 264 . . . . . . . . . . . . 13 |- ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> E. i e. Z x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
169, 15sylib 208 . . . . . . . . . . . 12 |- ( x e. D -> E. i e. Z x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
176, 16syl 17 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) -> E. i e. Z x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
18 nfv 1843 . . . . . . . . . . . . . . . . . . 19 |- F/ m ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A )
19 nfv 1843 . . . . . . . . . . . . . . . . . . 19 |- F/ m k e. NN
2018, 19nfan 1828 . . . . . . . . . . . . . . . . . 18 |- F/ m ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN )
21 nfv 1843 . . . . . . . . . . . . . . . . . 18 |- F/ m i e. Z
2220, 21nfan 1828 . . . . . . . . . . . . . . . . 17 |- F/ m ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z )
23 nfcv 2764 . . . . . . . . . . . . . . . . . 18 |- F/_ m x
24 nfii1 4551 . . . . . . . . . . . . . . . . . 18 |- F/_ m |^|_ m e. ( ZZ>= ` i ) dom ( F ` m )
2523, 24nfel 2777 . . . . . . . . . . . . . . . . 17 |- F/ m x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m )
2622, 25nfan 1828 . . . . . . . . . . . . . . . 16 |- F/ m ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
27 nfmpt1 4747 . . . . . . . . . . . . . . . 16 |- F/_ m ( m e. Z |-> ( ( F ` m ) ` x ) )
28 eqid 2622 . . . . . . . . . . . . . . . 16 |- ( ZZ>= ` i ) = ( ZZ>= ` i )
29 uzssz 11707 . . . . . . . . . . . . . . . . . . 19 |- ( ZZ>= ` M ) C_ ZZ
30 smflimlem2.1 . . . . . . . . . . . . . . . . . . . . 21 |- Z = ( ZZ>= ` M )
3130eleq2i 2693 . . . . . . . . . . . . . . . . . . . 20 |- ( i e. Z <-> i e. ( ZZ>= ` M ) )
3231biimpi 206 . . . . . . . . . . . . . . . . . . 19 |- ( i e. Z -> i e. ( ZZ>= ` M ) )
3329, 32sseldi 3601 . . . . . . . . . . . . . . . . . 18 |- ( i e. Z -> i e. ZZ )
34 uzid 11702 . . . . . . . . . . . . . . . . . 18 |- ( i e. ZZ -> i e. ( ZZ>= ` i ) )
3533, 34syl 17 . . . . . . . . . . . . . . . . 17 |- ( i e. Z -> i e. ( ZZ>= ` i ) )
3635ad2antlr 763 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) -> i e. ( ZZ>= ` i ) )
37 simplll 798 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ x e. D ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> ( ph /\ x e. D ) )
3837simpld 475 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ x e. D ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> ph )
39 uzss 11708 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. ( ZZ>= ` M ) -> ( ZZ>= ` i ) C_ ( ZZ>= ` M ) )
4032, 39syl 17 . . . . . . . . . . . . . . . . . . . . . 22 |- ( i e. Z -> ( ZZ>= ` i ) C_ ( ZZ>= ` M ) )
4140, 30syl6sseqr 3652 . . . . . . . . . . . . . . . . . . . . 21 |- ( i e. Z -> ( ZZ>= ` i ) C_ Z )
4241sselda 3603 . . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. Z /\ m e. ( ZZ>= ` i ) ) -> m e. Z )
4342ad4ant24 1298 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ x e. D ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> m e. Z )
44 eliinid 39294 . . . . . . . . . . . . . . . . . . . 20 |- ( ( x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) /\ m e. ( ZZ>= ` i ) ) -> x e. dom ( F ` m ) )
4544adantll 750 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ x e. D ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> x e. dom ( F ` m ) )
46 eqidd 2623 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` x ) ) )
47 fvexd 6203 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. Z ) -> ( ( F ` m ) ` x ) e. _V )
4846, 47fvmpt2d 6293 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ m e. Z ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) = ( ( F ` m ) ` x ) )
49483adant3 1081 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) = ( ( F ` m ) ` x ) )
50 smflimlem2.2 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> S e. SAlg )
5150adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. Z ) -> S e. SAlg )
52 smflimlem2.3 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> F : Z --> (SMblFn ` S ) )
5352ffvelrnda 6359 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. Z ) -> ( F ` m ) e. (SMblFn ` S ) )
54 eqid 2622 . . . . . . . . . . . . . . . . . . . . . . 23 |- dom ( F ` m ) = dom ( F ` m )
5551, 53, 54smff 40941 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
56553adant3 1081 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> ( F ` m ) : dom ( F ` m ) --> RR )
57 simp3 1063 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> x e. dom ( F ` m ) )
5856, 57ffvelrnd 6360 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> ( ( F ` m ) ` x ) e. RR )
5949, 58eqeltrd 2701 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) e. RR )
6038, 43, 45, 59syl3anc 1326 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ x e. D ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) e. RR )
6160ad5ant1345 1316 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) e. RR )
6261ad5ant1345 1316 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) e. RR )
631eleq2i 2693 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x e. D <-> x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } )
6463biimpi 206 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. D -> x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } )
65 rabidim2 39284 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } -> ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> )
6664, 65syl 17 . . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. D -> ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> )
67 climdm 14285 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> <-> ( m e. Z |-> ( ( F ` m ) ` x ) ) ~~> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
6866, 67sylib 208 . . . . . . . . . . . . . . . . . . . . 21 |- ( x e. D -> ( m e. Z |-> ( ( F ` m ) ` x ) ) ~~> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
6968adantl 482 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. D ) -> ( m e. Z |-> ( ( F ` m ) ` x ) ) ~~> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
7069, 67sylibr 224 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. D ) -> ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> )
7170, 67sylib 208 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. D ) -> ( m e. Z |-> ( ( F ` m ) ` x ) ) ~~> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
72 nfcv 2764 . . . . . . . . . . . . . . . . . . . 20 |- F/_ x F
73 smflimlem2.5 . . . . . . . . . . . . . . . . . . . 20 |- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
74 simpr 477 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. D ) -> x e. D )
753, 72, 73, 74fnlimfv 39895 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. D ) -> ( G ` x ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
7675eqcomd 2628 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. D ) -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( G ` x ) )
7771, 76breqtrd 4679 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. D ) -> ( m e. Z |-> ( ( F ` m ) ` x ) ) ~~> ( G ` x ) )
7877ad4antr 768 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) -> ( m e. Z |-> ( ( F ` m ) ` x ) ) ~~> ( G ` x ) )
79 smflimlem2.6 . . . . . . . . . . . . . . . . 17 |- ( ph -> A e. RR )
8079ad5antr 770 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) -> A e. RR )
81 simp-4r 807 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) -> ( G ` x ) <_ A )
82 simpllr 799 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) -> k e. NN )
83 nnrecrp 39605 . . . . . . . . . . . . . . . . 17 |- ( k e. NN -> ( 1 / k ) e. RR+ )
8482, 83syl 17 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) -> ( 1 / k ) e. RR+ )
8526, 27, 28, 36, 62, 78, 80, 81, 84climleltrp 39908 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) -> E. n e. ( ZZ>= ` i ) A. m e. ( ZZ>= ` n ) ( ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) e. RR /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) )
86 simp-6l 810 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ n e. ( ZZ>= ` i ) ) -> ph )
87 simplr 792 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) -> i e. Z )
8887adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ n e. ( ZZ>= ` i ) ) -> i e. Z )
89 simplr 792 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ n e. ( ZZ>= ` i ) ) -> x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
90 simpr 477 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ n e. ( ZZ>= ` i ) ) -> n e. ( ZZ>= ` i ) )
91 nfv 1843 . . . . . . . . . . . . . . . . . . . 20 |- F/ m ph
9291, 21, 25nf3an 1831 . . . . . . . . . . . . . . . . . . 19 |- F/ m ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
93 nfv 1843 . . . . . . . . . . . . . . . . . . 19 |- F/ m n e. ( ZZ>= ` i )
9492, 93nfan 1828 . . . . . . . . . . . . . . . . . 18 |- F/ m ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ n e. ( ZZ>= ` i ) )
95 simpll 790 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ n e. ( ZZ>= ` i ) ) /\ m e. ( ZZ>= ` n ) ) -> ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) )
9628uztrn2 11705 . . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. ( ZZ>= ` i ) /\ m e. ( ZZ>= ` n ) ) -> m e. ( ZZ>= ` i ) )
9796adantll 750 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ n e. ( ZZ>= ` i ) ) /\ m e. ( ZZ>= ` n ) ) -> m e. ( ZZ>= ` i ) )
98 simpll2 1101 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> i e. Z )
99 simplr 792 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> m e. ( ZZ>= ` i ) )
10098, 99, 42syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> m e. Z )
101 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) )
102 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( m e. Z -> m e. Z )
103 fvexd 6203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( m e. Z -> ( ( F ` m ) ` x ) e. _V )
104 eqid 2622 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` x ) )
105104fvmpt2 6291 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( m e. Z /\ ( ( F ` m ) ` x ) e. _V ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) = ( ( F ` m ) ` x ) )
106102, 103, 105syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( m e. Z -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) = ( ( F ` m ) ` x ) )
107106eqcomd 2628 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( m e. Z -> ( ( F ` m ) ` x ) = ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) )
108107adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( m e. Z /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> ( ( F ` m ) ` x ) = ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) )
109 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( m e. Z /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) )
110108, 109eqbrtrd 4675 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( m e. Z /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) )
111100, 101, 110syl2anc 693 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) )
112443ad2antl3 1225 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> x e. dom ( F ` m ) )
113112adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) /\ ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) ) -> x e. dom ( F ` m ) )
114 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) /\ ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) ) -> ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) )
115113, 114jca 554 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) /\ ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) ) -> ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) ) )
116 rabid 3116 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } <-> ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) ) )
117115, 116sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) /\ ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) ) -> x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } )
118111, 117syldan 487 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } )
119118adantrl 752 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) /\ ( ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) e. RR /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) ) -> x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } )
120119ex 450 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> ( ( ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) e. RR /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) )
12195, 97, 120syl2anc 693 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ n e. ( ZZ>= ` i ) ) /\ m e. ( ZZ>= ` n ) ) -> ( ( ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) e. RR /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) )
12294, 121ralimdaa 2958 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ n e. ( ZZ>= ` i ) ) -> ( A. m e. ( ZZ>= ` n ) ( ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) e. RR /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) )
12386, 88, 89, 90, 122syl31anc 1329 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ n e. ( ZZ>= ` i ) ) -> ( A. m e. ( ZZ>= ` n ) ( ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) e. RR /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) )
124123reximdva 3017 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) -> ( E. n e. ( ZZ>= ` i ) A. m e. ( ZZ>= ` n ) ( ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) e. RR /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> E. n e. ( ZZ>= ` i ) A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) )
12585, 124mpd 15 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) -> E. n e. ( ZZ>= ` i ) A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } )
126 ssrexv 3667 . . . . . . . . . . . . . . . 16 |- ( ( ZZ>= ` i ) C_ Z -> ( E. n e. ( ZZ>= ` i ) A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } -> E. n e. Z A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) )
12741, 126syl 17 . . . . . . . . . . . . . . 15 |- ( i e. Z -> ( E. n e. ( ZZ>= ` i ) A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } -> E. n e. Z A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) )
128127ad2antlr 763 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) -> ( E. n e. ( ZZ>= ` i ) A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } -> E. n e. Z A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) )
129125, 128mpd 15 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) -> E. n e. Z A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } )
130129ex 450 . . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) -> ( x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) -> E. n e. Z A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) )
131130rexlimdva 3031 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) -> ( E. i e. Z x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) -> E. n e. Z A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) )
13217, 131mpd 15 . . . . . . . . . 10 |- ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) -> E. n e. Z A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } )
133 nfv 1843 . . . . . . . . . . . . . . . 16 |- F/ m ( ph /\ k e. NN /\ n e. Z )
134 nfra1 2941 . . . . . . . . . . . . . . . 16 |- F/ m A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) }
135133, 134nfan 1828 . . . . . . . . . . . . . . 15 |- F/ m ( ( ph /\ k e. NN /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } )
136 simpll1 1100 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. NN /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) /\ m e. ( ZZ>= ` n ) ) -> ph )
137 simpll2 1101 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. NN /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) /\ m e. ( ZZ>= ` n ) ) -> k e. NN )
13830uztrn2 11705 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( n e. Z /\ j e. ( ZZ>= ` n ) ) -> j e. Z )
139138ssd 39252 . . . . . . . . . . . . . . . . . . . . 21 |- ( n e. Z -> ( ZZ>= ` n ) C_ Z )
140139sselda 3603 . . . . . . . . . . . . . . . . . . . 20 |- ( ( n e. Z /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
141140adantll 750 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( k e. NN /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
1421413adantl1 1217 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. NN /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
143142adantlr 751 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. NN /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
144 rspa 2930 . . . . . . . . . . . . . . . . . 18 |- ( ( A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } /\ m e. ( ZZ>= ` n ) ) -> x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } )
145144adantll 750 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ k e. NN /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) /\ m e. ( ZZ>= ` n ) ) -> x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } )
146 simp1 1061 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. NN /\ m e. Z ) -> ph )
147 simp3 1063 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN /\ m e. Z ) -> m e. Z )
148 simp2 1062 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN /\ m e. Z ) -> k e. NN )
149 eqid 2622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( 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 ) ) }
150149, 50rabexd 4814 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
151150ralrimivw 2967 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> A. k e. NN { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
152151ralrimivw 2967 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> A. m e. Z A. k e. NN { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
1531523ad2ant1 1082 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN /\ m e. Z ) -> A. m e. Z A. k e. NN { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
154 smflimlem2.7 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- P = ( 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 ) ) } )
155154elrnmpt2id 39427 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( m e. Z /\ k e. NN /\ A. m e. Z A. k e. NN { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V ) -> ( m P k ) e. ran P )
156147, 148, 153, 155syl3anc 1326 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. NN /\ m e. Z ) -> ( m P k ) e. ran P )
157 ovex 6678 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( m P k ) e. _V
158 eleq1 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( r = ( m P k ) -> ( r e. ran P <-> ( m P k ) e. ran P ) )
159158anbi2d 740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( r = ( m P k ) -> ( ( ph /\ r e. ran P ) <-> ( ph /\ ( m P k ) e. ran P ) ) )
160 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( r = ( m P k ) -> ( C ` r ) = ( C ` ( m P k ) ) )
161 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( r = ( m P k ) -> r = ( m P k ) )
162160, 161eleq12d 2695 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( r = ( m P k ) -> ( ( C ` r ) e. r <-> ( C ` ( m P k ) ) e. ( m P k ) ) )
163159, 162imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( r = ( m P k ) -> ( ( ( ph /\ r e. ran P ) -> ( C ` r ) e. r ) <-> ( ( ph /\ ( m P k ) e. ran P ) -> ( C ` ( m P k ) ) e. ( m P k ) ) ) )
164 smflimlem2.10 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ r e. ran P ) -> ( C ` r ) e. r )
165157, 163, 164vtocl 3259 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( m P k ) e. ran P ) -> ( C ` ( m P k ) ) e. ( m P k ) )
166146, 156, 165syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ k e. NN /\ m e. Z ) -> ( C ` ( m P k ) ) e. ( m P k ) )
167 fvexd 6203 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ k e. NN /\ m e. Z ) -> ( C ` ( m P k ) ) e. _V )
168 smflimlem2.8 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- H = ( m e. Z , k e. NN |-> ( C ` ( m P k ) ) )
169168ovmpt4g 6783 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( m e. Z /\ k e. NN /\ ( C ` ( m P k ) ) e. _V ) -> ( m H k ) = ( C ` ( m P k ) ) )
170147, 148, 167, 169syl3anc 1326 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN /\ m e. Z ) -> ( m H k ) = ( C ` ( m P k ) ) )
171170eqcomd 2628 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. NN /\ m e. Z ) -> ( C ` ( m P k ) ) = ( m H k ) )
172146, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ k e. NN /\ m e. Z ) -> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
173154ovmpt4g 6783 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 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 ) ) } e. _V ) -> ( m P k ) = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
174147, 148, 172, 173syl3anc 1326 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ k e. NN /\ m e. Z ) -> ( m P k ) = { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
175171, 174eleq12d 2695 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ k e. NN /\ m e. Z ) -> ( ( C ` ( m P k ) ) e. ( m P k ) <-> ( m H k ) e. { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } ) )
176166, 175mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. NN /\ m e. Z ) -> ( m H k ) e. { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } )
177 ineq1 3807 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s = ( m H k ) -> ( s i^i dom ( F ` m ) ) = ( ( m H k ) i^i dom ( F ` m ) ) )
178177eqeq2d 2632 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( s = ( m H k ) -> ( { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) <-> { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( ( m H k ) i^i dom ( F ` m ) ) ) )
179178elrab 3363 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( m H k ) e. { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } <-> ( ( m H k ) e. S /\ { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( ( m H k ) i^i dom ( F ` m ) ) ) )
180176, 179sylib 208 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. NN /\ m e. Z ) -> ( ( m H k ) e. S /\ { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( ( m H k ) i^i dom ( F ` m ) ) ) )
181180simprd 479 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. NN /\ m e. Z ) -> { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( ( m H k ) i^i dom ( F ` m ) ) )
182 inss1 3833 . . . . . . . . . . . . . . . . . . . 20 |- ( ( m H k ) i^i dom ( F ` m ) ) C_ ( m H k )
183181, 182syl6eqss 3655 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. NN /\ m e. Z ) -> { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } C_ ( m H k ) )
184183adantr 481 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. NN /\ m e. Z ) /\ x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) -> { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } C_ ( m H k ) )
185 simpr 477 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. NN /\ m e. Z ) /\ x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) -> x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } )
186184, 185sseldd 3604 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. NN /\ m e. Z ) /\ x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) -> x e. ( m H k ) )
187136, 137, 143, 145, 186syl31anc 1329 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ k e. NN /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) /\ m e. ( ZZ>= ` n ) ) -> x e. ( m H k ) )
188187ex 450 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. NN /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) -> ( m e. ( ZZ>= ` n ) -> x e. ( m H k ) ) )
189135, 188ralrimi 2957 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. NN /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) -> A. m e. ( ZZ>= ` n ) x e. ( m H k ) )
190 vex 3203 . . . . . . . . . . . . . . 15 |- x e. _V
191 eliin 4525 . . . . . . . . . . . . . . 15 |- ( x e. _V -> ( x e. |^|_ m e. ( ZZ>= ` n ) ( m H k ) <-> A. m e. ( ZZ>= ` n ) x e. ( m H k ) ) )
192190, 191ax-mp 5 . . . . . . . . . . . . . 14 |- ( x e. |^|_ m e. ( ZZ>= ` n ) ( m H k ) <-> A. m e. ( ZZ>= ` n ) x e. ( m H k ) )
193189, 192sylibr 224 . . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. NN /\ n e. Z ) /\ A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } ) -> x e. |^|_ m e. ( ZZ>= ` n ) ( m H k ) )
194193ex 450 . . . . . . . . . . . 12 |- ( ( ph /\ k e. NN /\ n e. Z ) -> ( A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } -> x e. |^|_ m e. ( ZZ>= ` n ) ( m H k ) ) )
195194ad5ant145 1315 . . . . . . . . . . 11 |- ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ n e. Z ) -> ( A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } -> x e. |^|_ m e. ( ZZ>= ` n ) ( m H k ) ) )
196195reximdva 3017 . . . . . . . . . 10 |- ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) -> ( E. n e. Z A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) ( m H k ) ) )
197132, 196mpd 15 . . . . . . . . 9 |- ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) -> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) ( m H k ) )
198 eliun 4524 . . . . . . . . 9 |- ( x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) <-> E. n e. Z x e. |^|_ m e. ( ZZ>= ` n ) ( m H k ) )
199197, 198sylibr 224 . . . . . . . 8 |- ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) )
200199ralrimiva 2966 . . . . . . 7 |- ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) -> A. k e. NN x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) )
201 eliin 4525 . . . . . . . 8 |- ( x e. _V -> ( x e. |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) <-> A. k e. NN x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) ) )
202190, 201ax-mp 5 . . . . . . 7 |- ( x e. |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) <-> A. k e. NN x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) )
203200, 202sylibr 224 . . . . . 6 |- ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) -> x e. |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) )
204 smflimlem2.9 . . . . . 6 |- I = |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k )
205203, 204syl6eleqr 2712 . . . . 5 |- ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) -> x e. I )
206205ex 450 . . . 4 |- ( ( ph /\ x e. D ) -> ( ( G ` x ) <_ A -> x e. I ) )
207206ralrimiva 2966 . . 3 |- ( ph -> A. x e. D ( ( G ` x ) <_ A -> x e. I ) )
208 rabss 3679 . . 3 |- ( { x e. D | ( G ` x ) <_ A } C_ I <-> A. x e. D ( ( G ` x ) <_ A -> x e. I ) )
209207, 208sylibr 224 . 2 |- ( ph -> { x e. D | ( G ` x ) <_ A } C_ I )
2105, 209ssind 3837 1 |- ( ph -> { x e. D | ( G ` x ) <_ A } C_ ( D i^i I ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   i^i cin 3573   C_ wss 3574   U_ciun 4520   |^|_ciin 4521   class class class wbr 4653   |-> cmpt 4729   dom cdm 5114   ran crn 5115   -->wf 5884   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   RRcr 9935   1c1 9937   + caddc 9939   < clt 10074   <_ cle 10075   / cdiv 10684   NNcn 11020   ZZcz 11377   ZZ>=cuz 11687   RR+crp 11832   ~~> cli 14215  SAlgcsalg 40528  SMblFncsmblfn 40909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-ioo 12179  df-ico 12181  df-fl 12593  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-rlim 14220  df-smblfn 40910
This theorem is referenced by:  smflimlem5  40983
  Copyright terms: Public domain W3C validator