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 sselid
 |-  ( 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 ) )