Metamath Proof Explorer

Theorem smflimlem2

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)

Ref Expression
Hypotheses 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 smflimlem2 
|- ( ph -> { x e. D | ( G ` x ) <_ A } C_ ( D i^i I ) )

Proof

Step Hyp Ref Expression
1 smflimlem2.1 
 |-  Z = ( ZZ>= ` M )
2 smflimlem2.2 
 |-  ( ph -> S e. SAlg )
3 smflimlem2.3 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
4 smflimlem2.4 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
5 smflimlem2.5 
 |-  G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
6 smflimlem2.6 
 |-  ( ph -> A e. RR )
7 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 ) ) } )
8 smflimlem2.8 
 |-  H = ( m e. Z , k e. NN |-> ( C ` ( m P k ) ) )
9 smflimlem2.9 
 |-  I = |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k )
10 smflimlem2.10 
 |-  ( ( ph /\ r e. ran P ) -> ( C ` r ) e. r )
11 nfrab1 
 |-  F/_ x { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
12 4 11 nfcxfr 
 |-  F/_ x D
13 12 ssrab2f 
 |-  { x e. D | ( G ` x ) <_ A } C_ D
14 13 a1i 
 |-  ( ph -> { x e. D | ( G ` x ) <_ A } C_ D )
15 simpllr 
 |-  ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) -> x e. D )
16 ssrab2 
 |-  { 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 )
17 4 16 eqsstri 
 |-  D C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
18 17 sseli 
 |-  ( x e. D -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
19 fveq2 
 |-  ( n = i -> ( ZZ>= ` n ) = ( ZZ>= ` i ) )
20 19 iineq1d 
 |-  ( n = i -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
21 20 cbviunv 
 |-  U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ i e. Z |^|_ m e. ( ZZ>= ` i ) dom ( F ` m )
22 21 eleq2i 
 |-  ( 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 ) )
23 eliun 
 |-  ( 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 ) )
24 22 23 bitri 
 |-  ( 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 ) )
25 18 24 sylib 
 |-  ( x e. D -> E. i e. Z x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
26 15 25 syl 
 |-  ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) -> E. i e. Z x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
27 nfv 
 |-  F/ m ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A )
28 nfv 
 |-  F/ m k e. NN
29 27 28 nfan 
 |-  F/ m ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN )
30 nfv 
 |-  F/ m i e. Z
31 29 30 nfan 
 |-  F/ m ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z )
32 nfcv 
 |-  F/_ m x
33 nfii1 
 |-  F/_ m |^|_ m e. ( ZZ>= ` i ) dom ( F ` m )
34 32 33 nfel 
 |-  F/ m x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m )
35 31 34 nfan 
 |-  F/ m ( ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
36 nfmpt1 
 |-  F/_ m ( m e. Z |-> ( ( F ` m ) ` x ) )
37 eqid 
 |-  ( ZZ>= ` i ) = ( ZZ>= ` i )
38 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
39 1 eleq2i 
 |-  ( i e. Z <-> i e. ( ZZ>= ` M ) )
40 39 biimpi 
 |-  ( i e. Z -> i e. ( ZZ>= ` M ) )
41 38 40 sseldi 
 |-  ( i e. Z -> i e. ZZ )
42 uzid 
 |-  ( i e. ZZ -> i e. ( ZZ>= ` i ) )
43 41 42 syl 
 |-  ( i e. Z -> i e. ( ZZ>= ` i ) )
44 43 ad2antlr 
 |-  ( ( ( ( ( ( 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 ) )
45 simplll 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> ( ph /\ x e. D ) )
46 45 simpld 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> ph )
47 uzss 
 |-  ( i e. ( ZZ>= ` M ) -> ( ZZ>= ` i ) C_ ( ZZ>= ` M ) )
48 40 47 syl 
 |-  ( i e. Z -> ( ZZ>= ` i ) C_ ( ZZ>= ` M ) )
49 48 1 sseqtrrdi 
 |-  ( i e. Z -> ( ZZ>= ` i ) C_ Z )
50 49 sselda 
 |-  ( ( i e. Z /\ m e. ( ZZ>= ` i ) ) -> m e. Z )
51 50 ad4ant24 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ i e. Z ) /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> m e. Z )
52 eliinid 
 |-  ( ( x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) /\ m e. ( ZZ>= ` i ) ) -> x e. dom ( F ` m ) )
53 52 adantll 
 |-  ( ( ( ( ( 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 ) )
54 eqidd 
 |-  ( ph -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` x ) ) )
55 fvexd 
 |-  ( ( ph /\ m e. Z ) -> ( ( F ` m ) ` x ) e. _V )
56 54 55 fvmpt2d 
 |-  ( ( ph /\ m e. Z ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) = ( ( F ` m ) ` x ) )
57 56 3adant3 
 |-  ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) = ( ( F ` m ) ` x ) )
58 2 adantr 
 |-  ( ( ph /\ m e. Z ) -> S e. SAlg )
59 3 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 3adant3 
 |-  ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> ( F ` m ) : dom ( F ` m ) --> RR )
63 simp3 
 |-  ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> x e. dom ( F ` m ) )
64 62 63 ffvelrnd 
 |-  ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> ( ( F ` m ) ` x ) e. RR )
65 57 64 eqeltrd 
 |-  ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) e. RR )
66 46 51 53 65 syl3anc 
 |-  ( ( ( ( ( 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 )
67 66 adantl3r 
 |-  ( ( ( ( ( ( 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 )
68 67 adantl3r 
 |-  ( ( ( ( ( ( ( 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 )
69 4 eleq2i 
 |-  ( 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 ~~> } )
70 69 biimpi 
 |-  ( 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 ~~> } )
71 rabidim2 
 |-  ( 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 ~~> )
72 70 71 syl 
 |-  ( x e. D -> ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> )
73 climdm 
 |-  ( ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> <-> ( m e. Z |-> ( ( F ` m ) ` x ) ) ~~> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
74 72 73 sylib 
 |-  ( x e. D -> ( m e. Z |-> ( ( F ` m ) ` x ) ) ~~> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
75 74 adantl 
 |-  ( ( ph /\ x e. D ) -> ( m e. Z |-> ( ( F ` m ) ` x ) ) ~~> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
76 75 73 sylibr 
 |-  ( ( ph /\ x e. D ) -> ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> )
77 76 73 sylib 
 |-  ( ( ph /\ x e. D ) -> ( m e. Z |-> ( ( F ` m ) ` x ) ) ~~> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
78 nfcv 
 |-  F/_ x F
79 simpr 
 |-  ( ( ph /\ x e. D ) -> x e. D )
80 12 78 5 79 fnlimfv 
 |-  ( ( ph /\ x e. D ) -> ( G ` x ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
81 80 eqcomd 
 |-  ( ( ph /\ x e. D ) -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( G ` x ) )
82 77 81 breqtrd 
 |-  ( ( ph /\ x e. D ) -> ( m e. Z |-> ( ( F ` m ) ` x ) ) ~~> ( G ` x ) )
83 82 ad4antr 
 |-  ( ( ( ( ( ( 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 ) )
84 6 ad5antr 
 |-  ( ( ( ( ( ( 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 )
85 simp-4r 
 |-  ( ( ( ( ( ( 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 )
86 simpllr 
 |-  ( ( ( ( ( ( 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 )
87 nnrecrp 
 |-  ( k e. NN -> ( 1 / k ) e. RR+ )
88 86 87 syl 
 |-  ( ( ( ( ( ( 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+ )
89 35 36 37 44 68 83 84 85 88 climleltrp 
 |-  ( ( ( ( ( ( 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 ) ) ) )
90 simp-6l 
 |-  ( ( ( ( ( ( ( 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 )
91 simplr 
 |-  ( ( ( ( ( ( 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 )
92 91 adantr 
 |-  ( ( ( ( ( ( ( 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 )
93 simplr 
 |-  ( ( ( ( ( ( ( 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 ) )
94 simpr 
 |-  ( ( ( ( ( ( ( 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 ) )
95 nfv 
 |-  F/ m ph
96 95 30 34 nf3an 
 |-  F/ m ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) )
97 nfv 
 |-  F/ m n e. ( ZZ>= ` i )
98 96 97 nfan 
 |-  F/ m ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ n e. ( ZZ>= ` i ) )
99 simpll 
 |-  ( ( ( ( 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 ) ) )
100 37 uztrn2 
 |-  ( ( n e. ( ZZ>= ` i ) /\ m e. ( ZZ>= ` n ) ) -> m e. ( ZZ>= ` i ) )
101 100 adantll 
 |-  ( ( ( ( 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 ) )
102 simpll2 
 |-  ( ( ( ( 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 )
103 simplr 
 |-  ( ( ( ( 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 ) )
104 102 103 50 syl2anc 
 |-  ( ( ( ( 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 )
105 simpr 
 |-  ( ( ( ( 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 ) ) )
106 id 
 |-  ( m e. Z -> m e. Z )
107 fvexd 
 |-  ( m e. Z -> ( ( F ` m ) ` x ) e. _V )
108 eqid 
 |-  ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` x ) )
109 108 fvmpt2 
 |-  ( ( m e. Z /\ ( ( F ` m ) ` x ) e. _V ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) = ( ( F ` m ) ` x ) )
110 106 107 109 syl2anc 
 |-  ( m e. Z -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) = ( ( F ` m ) ` x ) )
111 110 eqcomd 
 |-  ( m e. Z -> ( ( F ` m ) ` x ) = ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) )
112 111 adantr 
 |-  ( ( m e. Z /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> ( ( F ` m ) ` x ) = ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) )
113 simpr 
 |-  ( ( m e. Z /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) )
114 112 113 eqbrtrd 
 |-  ( ( m e. Z /\ ( ( m e. Z |-> ( ( F ` m ) ` x ) ) ` m ) < ( A + ( 1 / k ) ) ) -> ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) )
115 104 105 114 syl2anc 
 |-  ( ( ( ( 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 ) ) )
116 52 3ad2antl3 
 |-  ( ( ( ph /\ i e. Z /\ x e. |^|_ m e. ( ZZ>= ` i ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` i ) ) -> x e. dom ( F ` m ) )
117 116 adantr 
 |-  ( ( ( ( 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 ) )
118 simpr 
 |-  ( ( ( ( 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 ) ) )
119 117 118 jca 
 |-  ( ( ( ( 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 ) ) ) )
120 rabid 
 |-  ( x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } <-> ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) ) )
121 119 120 sylibr 
 |-  ( ( ( ( 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 ) ) } )
122 115 121 syldan 
 |-  ( ( ( ( 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 ) ) } )
123 122 adantrl 
 |-  ( ( ( ( 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 ) ) } )
124 123 ex 
 |-  ( ( ( 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 ) ) } ) )
125 99 101 124 syl2anc 
 |-  ( ( ( ( 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 ) ) } ) )
126 98 125 ralimdaa 
 |-  ( ( ( 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 ) ) } ) )
127 90 92 93 94 126 syl31anc 
 |-  ( ( ( ( ( ( ( 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 ) ) } ) )
128 127 reximdva 
 |-  ( ( ( ( ( ( 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 ) ) } ) )
129 89 128 mpd 
 |-  ( ( ( ( ( ( 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 ) ) } )
130 ssrexv 
 |-  ( ( 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 ) ) } ) )
131 49 130 syl 
 |-  ( 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 ) ) } ) )
132 131 ad2antlr 
 |-  ( ( ( ( ( ( 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 ) ) } ) )
133 129 132 mpd 
 |-  ( ( ( ( ( ( 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 ) ) } )
134 133 rexlimdva2 
 |-  ( ( ( ( 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 ) ) } ) )
135 26 134 mpd 
 |-  ( ( ( ( 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 ) ) } )
136 nfv 
 |-  F/ m ( ph /\ k e. NN /\ n e. Z )
137 nfra1 
 |-  F/ m A. m e. ( ZZ>= ` n ) x e. { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) }
138 136 137 nfan 
 |-  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 ) ) } )
139 simpll1 
 |-  ( ( ( ( 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 )
140 simpll2 
 |-  ( ( ( ( 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 )
141 1 uztrn2 
 |-  ( ( n e. Z /\ j e. ( ZZ>= ` n ) ) -> j e. Z )
142 141 ssd 
 |-  ( n e. Z -> ( ZZ>= ` n ) C_ Z )
143 142 sselda 
 |-  ( ( n e. Z /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
144 143 adantll 
 |-  ( ( ( k e. NN /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
145 144 3adantl1 
 |-  ( ( ( ph /\ k e. NN /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
146 145 adantlr 
 |-  ( ( ( ( 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 )
147 rspa 
 |-  ( ( 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 ) ) } )
148 147 adantll 
 |-  ( ( ( ( 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 ) ) } )
149 simp1 
 |-  ( ( ph /\ k e. NN /\ m e. Z ) -> ph )
150 simp3 
 |-  ( ( ph /\ k e. NN /\ m e. Z ) -> m e. Z )
151 simp2 
 |-  ( ( ph /\ k e. NN /\ m e. Z ) -> k e. NN )
152 eqid 
 |-  { 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 ) ) }
153 152 2 rabexd 
 |-  ( ph -> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } e. _V )
154 153 ralrimivw 
 |-  ( 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 )
155 154 ralrimivw 
 |-  ( 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 )
156 155 3ad2ant1 
 |-  ( ( 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 )
157 7 elrnmpoid 
 |-  ( ( 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 )
158 150 151 156 157 syl3anc 
 |-  ( ( ph /\ k e. NN /\ m e. Z ) -> ( m P k ) e. ran P )
159 ovex 
 |-  ( m P k ) e. _V
160 eleq1 
 |-  ( r = ( m P k ) -> ( r e. ran P <-> ( m P k ) e. ran P ) )
161 160 anbi2d 
 |-  ( r = ( m P k ) -> ( ( ph /\ r e. ran P ) <-> ( ph /\ ( m P k ) e. ran P ) ) )
162 fveq2 
 |-  ( r = ( m P k ) -> ( C ` r ) = ( C ` ( m P k ) ) )
163 id 
 |-  ( r = ( m P k ) -> r = ( m P k ) )
164 162 163 eleq12d 
 |-  ( r = ( m P k ) -> ( ( C ` r ) e. r <-> ( C ` ( m P k ) ) e. ( m P k ) ) )
165 161 164 imbi12d 
 |-  ( 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 ) ) ) )
166 159 165 10 vtocl 
 |-  ( ( ph /\ ( m P k ) e. ran P ) -> ( C ` ( m P k ) ) e. ( m P k ) )
167 149 158 166 syl2anc 
 |-  ( ( ph /\ k e. NN /\ m e. Z ) -> ( C ` ( m P k ) ) e. ( m P k ) )
168 fvexd 
 |-  ( ( ph /\ k e. NN /\ m e. Z ) -> ( C ` ( m P k ) ) e. _V )
169 8 ovmpt4g 
 |-  ( ( m e. Z /\ k e. NN /\ ( C ` ( m P k ) ) e. _V ) -> ( m H k ) = ( C ` ( m P k ) ) )
170 150 151 168 169 syl3anc 
 |-  ( ( ph /\ k e. NN /\ m e. Z ) -> ( m H k ) = ( C ` ( m P k ) ) )
171 170 eqcomd 
 |-  ( ( ph /\ k e. NN /\ m e. Z ) -> ( C ` ( m P k ) ) = ( m H k ) )
172 149 153 syl 
 |-  ( ( 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 )
173 7 ovmpt4g 
 |-  ( ( 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 ) ) } )
174 150 151 172 173 syl3anc 
 |-  ( ( 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 ) ) } )
175 171 174 eleq12d 
 |-  ( ( 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 ) ) } ) )
176 167 175 mpbid 
 |-  ( ( 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 
 |-  ( s = ( m H k ) -> ( s i^i dom ( F ` m ) ) = ( ( m H k ) i^i dom ( F ` m ) ) )
178 177 eqeq2d 
 |-  ( 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 ) ) ) )
179 178 elrab 
 |-  ( ( 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 ) ) ) )
180 176 179 sylib 
 |-  ( ( 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 ) ) ) )
181 180 simprd 
 |-  ( ( 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 
 |-  ( ( m H k ) i^i dom ( F ` m ) ) C_ ( m H k )
183 181 182 eqsstrdi 
 |-  ( ( ph /\ k e. NN /\ m e. Z ) -> { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } C_ ( m H k ) )
184 183 adantr 
 |-  ( ( ( 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 
 |-  ( ( ( 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 ) ) } )
186 184 185 sseldd 
 |-  ( ( ( 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 ) )
187 139 140 146 148 186 syl31anc 
 |-  ( ( ( ( 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 ) )
188 187 ex 
 |-  ( ( ( 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 ) ) )
189 138 188 ralrimi 
 |-  ( ( ( 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 
 |-  x e. _V
191 eliin 
 |-  ( x e. _V -> ( x e. |^|_ m e. ( ZZ>= ` n ) ( m H k ) <-> A. m e. ( ZZ>= ` n ) x e. ( m H k ) ) )
192 190 191 ax-mp 
 |-  ( x e. |^|_ m e. ( ZZ>= ` n ) ( m H k ) <-> A. m e. ( ZZ>= ` n ) x e. ( m H k ) )
193 189 192 sylibr 
 |-  ( ( ( 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 ) )
194 193 ex 
 |-  ( ( 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 ) ) )
195 194 ad5ant145 
 |-  ( ( ( ( ( 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 ) ) )
196 195 reximdva 
 |-  ( ( ( ( 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 ) ) )
197 135 196 mpd 
 |-  ( ( ( ( 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 
 |-  ( 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 ) )
199 197 198 sylibr 
 |-  ( ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) /\ k e. NN ) -> x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) )
200 199 ralrimiva 
 |-  ( ( ( 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 
 |-  ( 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 ) ) )
202 190 201 ax-mp 
 |-  ( 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 ) )
203 200 202 sylibr 
 |-  ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) -> x e. |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) )
204 203 9 eleqtrrdi 
 |-  ( ( ( ph /\ x e. D ) /\ ( G ` x ) <_ A ) -> x e. I )
205 204 ex 
 |-  ( ( ph /\ x e. D ) -> ( ( G ` x ) <_ A -> x e. I ) )
206 205 ralrimiva 
 |-  ( ph -> A. x e. D ( ( G ` x ) <_ A -> x e. I ) )
207 rabss 
 |-  ( { x e. D | ( G ` x ) <_ A } C_ I <-> A. x e. D ( ( G ` x ) <_ A -> x e. I ) )
208 206 207 sylibr 
 |-  ( ph -> { x e. D | ( G ` x ) <_ A } C_ I )
209 14 208 ssind 
 |-  ( ph -> { x e. D | ( G ` x ) <_ A } C_ ( D i^i I ) )