Metamath Proof Explorer

Theorem smflimlem4

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 smflimlem4.1 
|- ( ph -> M e. ZZ )
smflimlem4.2 
|- Z = ( ZZ>= ` M )
smflimlem4.3 
|- ( ph -> S e. SAlg )
smflimlem4.4 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smflimlem4.5 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
smflimlem4.6 
|- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
smflimlem4.7 
|- ( ph -> A e. RR )
smflimlem4.8 
|- 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 ) ) } )
smflimlem4.9 
|- H = ( m e. Z , k e. NN |-> ( C ` ( m P k ) ) )
smflimlem4.10 
|- I = |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k )
smflimlem4.11 
|- ( ( ph /\ r e. ran P ) -> ( C ` r ) e. r )
Assertion smflimlem4 
|- ( ph -> ( D i^i I ) C_ { x e. D | ( G ` x ) <_ A } )

Proof

Step Hyp Ref Expression
1 smflimlem4.1 
 |-  ( ph -> M e. ZZ )
2 smflimlem4.2 
 |-  Z = ( ZZ>= ` M )
3 smflimlem4.3 
 |-  ( ph -> S e. SAlg )
4 smflimlem4.4 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
5 smflimlem4.5 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
6 smflimlem4.6 
 |-  G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
7 smflimlem4.7 
 |-  ( ph -> A e. RR )
8 smflimlem4.8 
 |-  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 ) ) } )
9 smflimlem4.9 
 |-  H = ( m e. Z , k e. NN |-> ( C ` ( m P k ) ) )
10 smflimlem4.10 
 |-  I = |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k )
11 smflimlem4.11 
 |-  ( ( ph /\ r e. ran P ) -> ( C ` r ) e. r )
12 inss1 
 |-  ( D i^i I ) C_ D
13 12 a1i 
 |-  ( ph -> ( D i^i I ) C_ D )
14 13 sselda 
 |-  ( ( ph /\ x e. ( D i^i I ) ) -> x e. D )
15 6 a1i 
 |-  ( ph -> G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) )
16 nfv 
 |-  F/ m ( ph /\ x e. D )
17 nfcv 
 |-  F/_ m F
18 nfcv 
 |-  F/_ z F
19 3 adantr 
 |-  ( ( ph /\ m e. Z ) -> S e. SAlg )
20 4 ffvelcdmda 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
21 eqid 
 |-  dom ( F ` m ) = dom ( F ` m )
22 19 20 21 smff 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
23 22 adantlr 
 |-  ( ( ( ph /\ x e. D ) /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
24 fveq2 
 |-  ( x = z -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` z ) )
25 24 mpteq2dv 
 |-  ( x = z -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` z ) ) )
26 25 eleq1d 
 |-  ( x = z -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> <-> ( m e. Z |-> ( ( F ` m ) ` z ) ) e. dom ~~> ) )
27 26 cbvrabv 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } = { z e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` z ) ) e. dom ~~> }
28 5 27 eqtri 
 |-  D = { z e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` z ) ) e. dom ~~> }
29 simpr 
 |-  ( ( ph /\ x e. D ) -> x e. D )
30 16 17 18 2 23 28 29 fnlimfvre 
 |-  ( ( ph /\ x e. D ) -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )
31 30 elexd 
 |-  ( ( ph /\ x e. D ) -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. _V )
32 15 31 fvmpt2d 
 |-  ( ( ph /\ x e. D ) -> ( G ` x ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
33 32 30 eqeltrd 
 |-  ( ( ph /\ x e. D ) -> ( G ` x ) e. RR )
34 14 33 syldan 
 |-  ( ( ph /\ x e. ( D i^i I ) ) -> ( G ` x ) e. RR )
35 34 adantr 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> ( G ` x ) e. RR )
36 7 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> A e. RR )
37 rpre 
 |-  ( y e. RR+ -> y e. RR )
38 37 adantl 
 |-  ( ( ph /\ y e. RR+ ) -> y e. RR )
39 36 38 readdcld 
 |-  ( ( ph /\ y e. RR+ ) -> ( A + y ) e. RR )
40 39 adantlr 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> ( A + y ) e. RR )
41 nfv 
 |-  F/ m ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ )
42 rphalfcl 
 |-  ( y e. RR+ -> ( y / 2 ) e. RR+ )
43 rpgtrecnn 
 |-  ( ( y / 2 ) e. RR+ -> E. k e. NN ( 1 / k ) < ( y / 2 ) )
44 42 43 syl 
 |-  ( y e. RR+ -> E. k e. NN ( 1 / k ) < ( y / 2 ) )
45 44 adantl 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> E. k e. NN ( 1 / k ) < ( y / 2 ) )
46 3 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ k e. NN ) /\ ( 1 / k ) < ( y / 2 ) ) -> S e. SAlg )
47 20 adantlr 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
48 47 ad5ant15 
 |-  ( ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ k e. NN ) /\ ( 1 / k ) < ( y / 2 ) ) /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
49 7 adantr 
 |-  ( ( ph /\ x e. ( D i^i I ) ) -> A e. RR )
50 49 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ k e. NN ) /\ ( 1 / k ) < ( y / 2 ) ) -> A e. RR )
51 nfcv 
 |-  F/_ k Z
52 nfcv 
 |-  F/_ j Z
53 nfcv 
 |-  F/_ j { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) }
54 nfcv 
 |-  F/_ k { s e. S | { z e. dom ( F ` m ) | ( ( F ` m ) ` z ) < ( A + ( 1 / j ) ) } = ( s i^i dom ( F ` m ) ) }
55 24 breq1d 
 |-  ( x = z -> ( ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) <-> ( ( F ` m ) ` z ) < ( A + ( 1 / k ) ) ) )
56 55 cbvrabv 
 |-  { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = { z e. dom ( F ` m ) | ( ( F ` m ) ` z ) < ( A + ( 1 / k ) ) }
57 56 a1i 
 |-  ( k = j -> { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = { z e. dom ( F ` m ) | ( ( F ` m ) ` z ) < ( A + ( 1 / k ) ) } )
58 oveq2 
 |-  ( k = j -> ( 1 / k ) = ( 1 / j ) )
59 58 oveq2d 
 |-  ( k = j -> ( A + ( 1 / k ) ) = ( A + ( 1 / j ) ) )
60 59 breq2d 
 |-  ( k = j -> ( ( ( F ` m ) ` z ) < ( A + ( 1 / k ) ) <-> ( ( F ` m ) ` z ) < ( A + ( 1 / j ) ) ) )
61 60 rabbidv 
 |-  ( k = j -> { z e. dom ( F ` m ) | ( ( F ` m ) ` z ) < ( A + ( 1 / k ) ) } = { z e. dom ( F ` m ) | ( ( F ` m ) ` z ) < ( A + ( 1 / j ) ) } )
62 57 61 eqtrd 
 |-  ( k = j -> { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = { z e. dom ( F ` m ) | ( ( F ` m ) ` z ) < ( A + ( 1 / j ) ) } )
63 62 eqeq1d 
 |-  ( k = j -> ( { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) <-> { z e. dom ( F ` m ) | ( ( F ` m ) ` z ) < ( A + ( 1 / j ) ) } = ( s i^i dom ( F ` m ) ) ) )
64 63 rabbidv 
 |-  ( k = j -> { s e. S | { x e. dom ( F ` m ) | ( ( F ` m ) ` x ) < ( A + ( 1 / k ) ) } = ( s i^i dom ( F ` m ) ) } = { s e. S | { z e. dom ( F ` m ) | ( ( F ` m ) ` z ) < ( A + ( 1 / j ) ) } = ( s i^i dom ( F ` m ) ) } )
65 51 52 53 54 64 cbvmpo2 
 |-  ( 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 ) ) } ) = ( m e. Z , j e. NN |-> { s e. S | { z e. dom ( F ` m ) | ( ( F ` m ) ` z ) < ( A + ( 1 / j ) ) } = ( s i^i dom ( F ` m ) ) } )
66 8 65 eqtri 
 |-  P = ( m e. Z , j e. NN |-> { s e. S | { z e. dom ( F ` m ) | ( ( F ` m ) ` z ) < ( A + ( 1 / j ) ) } = ( s i^i dom ( F ` m ) ) } )
67 nfcv 
 |-  F/_ j ( C ` ( m P k ) )
68 nfcv 
 |-  F/_ k ( C ` ( m P j ) )
69 oveq2 
 |-  ( k = j -> ( m P k ) = ( m P j ) )
70 69 fveq2d 
 |-  ( k = j -> ( C ` ( m P k ) ) = ( C ` ( m P j ) ) )
71 51 52 67 68 70 cbvmpo2 
 |-  ( m e. Z , k e. NN |-> ( C ` ( m P k ) ) ) = ( m e. Z , j e. NN |-> ( C ` ( m P j ) ) )
72 9 71 eqtri 
 |-  H = ( m e. Z , j e. NN |-> ( C ` ( m P j ) ) )
73 simpll 
 |-  ( ( ( k = j /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> k = j )
74 73 oveq2d 
 |-  ( ( ( k = j /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( m H k ) = ( m H j ) )
75 74 iineq2dv 
 |-  ( ( k = j /\ n e. Z ) -> |^|_ m e. ( ZZ>= ` n ) ( m H k ) = |^|_ m e. ( ZZ>= ` n ) ( m H j ) )
76 75 iuneq2dv 
 |-  ( k = j -> U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H j ) )
77 76 cbviinv 
 |-  |^|_ k e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H k ) = |^|_ j e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H j )
78 10 77 eqtri 
 |-  I = |^|_ j e. NN U_ n e. Z |^|_ m e. ( ZZ>= ` n ) ( m H j )
79 11 adantlr 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ r e. ran P ) -> ( C ` r ) e. r )
80 79 ad5ant15 
 |-  ( ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ k e. NN ) /\ ( 1 / k ) < ( y / 2 ) ) /\ r e. ran P ) -> ( C ` r ) e. r )
81 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ k e. NN ) /\ ( 1 / k ) < ( y / 2 ) ) -> x e. ( D i^i I ) )
82 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ k e. NN ) /\ ( 1 / k ) < ( y / 2 ) ) -> k e. NN )
83 42 ad3antlr 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ k e. NN ) /\ ( 1 / k ) < ( y / 2 ) ) -> ( y / 2 ) e. RR+ )
84 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ k e. NN ) /\ ( 1 / k ) < ( y / 2 ) ) -> ( 1 / k ) < ( y / 2 ) )
85 2 46 48 28 50 66 72 78 80 81 82 83 84 smflimlem3 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ k e. NN ) /\ ( 1 / k ) < ( y / 2 ) ) -> E. m e. Z A. i e. ( ZZ>= ` m ) ( x e. dom ( F ` i ) /\ ( ( F ` i ) ` x ) < ( A + ( y / 2 ) ) ) )
86 85 rexlimdva2 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> ( E. k e. NN ( 1 / k ) < ( y / 2 ) -> E. m e. Z A. i e. ( ZZ>= ` m ) ( x e. dom ( F ` i ) /\ ( ( F ` i ) ` x ) < ( A + ( y / 2 ) ) ) ) )
87 45 86 mpd 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> E. m e. Z A. i e. ( ZZ>= ` m ) ( x e. dom ( F ` i ) /\ ( ( F ` i ) ` x ) < ( A + ( y / 2 ) ) ) )
88 nfv 
 |-  F/ i ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ )
89 nfcv 
 |-  F/_ i F
90 nfcv 
 |-  F/_ x F
91 1 ad2antrr 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> M e. ZZ )
92 eleq1w 
 |-  ( m = i -> ( m e. Z <-> i e. Z ) )
93 92 anbi2d 
 |-  ( m = i -> ( ( ph /\ m e. Z ) <-> ( ph /\ i e. Z ) ) )
94 fveq2 
 |-  ( m = i -> ( F ` m ) = ( F ` i ) )
95 94 dmeqd 
 |-  ( m = i -> dom ( F ` m ) = dom ( F ` i ) )
96 94 95 feq12d 
 |-  ( m = i -> ( ( F ` m ) : dom ( F ` m ) --> RR <-> ( F ` i ) : dom ( F ` i ) --> RR ) )
97 93 96 imbi12d 
 |-  ( m = i -> ( ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR ) <-> ( ( ph /\ i e. Z ) -> ( F ` i ) : dom ( F ` i ) --> RR ) ) )
98 97 22 chvarvv 
 |-  ( ( ph /\ i e. Z ) -> ( F ` i ) : dom ( F ` i ) --> RR )
99 98 ad4ant14 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ i e. Z ) -> ( F ` i ) : dom ( F ` i ) --> RR )
100 fveq2 
 |-  ( m = l -> ( F ` m ) = ( F ` l ) )
101 100 dmeqd 
 |-  ( m = l -> dom ( F ` m ) = dom ( F ` l ) )
102 101 cbviinv 
 |-  |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ l e. ( ZZ>= ` n ) dom ( F ` l )
103 102 a1i 
 |-  ( n e. Z -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ l e. ( ZZ>= ` n ) dom ( F ` l ) )
104 103 iuneq2i 
 |-  U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ n e. Z |^|_ l e. ( ZZ>= ` n ) dom ( F ` l )
105 fveq2 
 |-  ( n = m -> ( ZZ>= ` n ) = ( ZZ>= ` m ) )
106 105 iineq1d 
 |-  ( n = m -> |^|_ l e. ( ZZ>= ` n ) dom ( F ` l ) = |^|_ l e. ( ZZ>= ` m ) dom ( F ` l ) )
107 fveq2 
 |-  ( l = i -> ( F ` l ) = ( F ` i ) )
108 107 dmeqd 
 |-  ( l = i -> dom ( F ` l ) = dom ( F ` i ) )
109 108 cbviinv 
 |-  |^|_ l e. ( ZZ>= ` m ) dom ( F ` l ) = |^|_ i e. ( ZZ>= ` m ) dom ( F ` i )
110 109 a1i 
 |-  ( n = m -> |^|_ l e. ( ZZ>= ` m ) dom ( F ` l ) = |^|_ i e. ( ZZ>= ` m ) dom ( F ` i ) )
111 106 110 eqtrd 
 |-  ( n = m -> |^|_ l e. ( ZZ>= ` n ) dom ( F ` l ) = |^|_ i e. ( ZZ>= ` m ) dom ( F ` i ) )
112 111 cbviunv 
 |-  U_ n e. Z |^|_ l e. ( ZZ>= ` n ) dom ( F ` l ) = U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i )
113 104 112 eqtri 
 |-  U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i )
114 113 rabeqi 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } = { x e. U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
115 fveq2 
 |-  ( i = m -> ( F ` i ) = ( F ` m ) )
116 115 fveq1d 
 |-  ( i = m -> ( ( F ` i ) ` x ) = ( ( F ` m ) ` x ) )
117 116 cbvmptv 
 |-  ( i e. Z |-> ( ( F ` i ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` x ) )
118 117 eqcomi 
 |-  ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( i e. Z |-> ( ( F ` i ) ` x ) )
119 118 eleq1i 
 |-  ( ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> <-> ( i e. Z |-> ( ( F ` i ) ` x ) ) e. dom ~~> )
120 119 rabbii 
 |-  { x e. U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } = { x e. U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i ) | ( i e. Z |-> ( ( F ` i ) ` x ) ) e. dom ~~> }
121 5 114 120 3eqtri 
 |-  D = { x e. U_ m e. Z |^|_ i e. ( ZZ>= ` m ) dom ( F ` i ) | ( i e. Z |-> ( ( F ` i ) ` x ) ) e. dom ~~> }
122 118 fveq2i 
 |-  ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( ~~> ` ( i e. Z |-> ( ( F ` i ) ` x ) ) )
123 122 mpteq2i 
 |-  ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) = ( x e. D |-> ( ~~> ` ( i e. Z |-> ( ( F ` i ) ` x ) ) ) )
124 6 123 eqtri 
 |-  G = ( x e. D |-> ( ~~> ` ( i e. Z |-> ( ( F ` i ) ` x ) ) ) )
125 14 adantr 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> x e. D )
126 42 adantl 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> ( y / 2 ) e. RR+ )
127 88 89 90 91 2 99 121 124 125 126 fnlimabslt 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> E. m e. Z A. i e. ( ZZ>= ` m ) ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) )
128 35 adantr 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( F ` i ) ` x ) e. RR ) -> ( G ` x ) e. RR )
129 simpr 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( F ` i ) ` x ) e. RR ) -> ( ( F ` i ) ` x ) e. RR )
130 128 129 resubcld 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( F ` i ) ` x ) e. RR ) -> ( ( G ` x ) - ( ( F ` i ) ` x ) ) e. RR )
131 130 adantrr 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( ( G ` x ) - ( ( F ` i ) ` x ) ) e. RR )
132 130 recnd 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( F ` i ) ` x ) e. RR ) -> ( ( G ` x ) - ( ( F ` i ) ` x ) ) e. CC )
133 132 abscld 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( F ` i ) ` x ) e. RR ) -> ( abs ` ( ( G ` x ) - ( ( F ` i ) ` x ) ) ) e. RR )
134 133 adantrr 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( abs ` ( ( G ` x ) - ( ( F ` i ) ` x ) ) ) e. RR )
135 37 rehalfcld 
 |-  ( y e. RR+ -> ( y / 2 ) e. RR )
136 135 ad2antlr 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( y / 2 ) e. RR )
137 131 leabsd 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( ( G ` x ) - ( ( F ` i ) ` x ) ) <_ ( abs ` ( ( G ` x ) - ( ( F ` i ) ` x ) ) ) )
138 34 recnd 
 |-  ( ( ph /\ x e. ( D i^i I ) ) -> ( G ` x ) e. CC )
139 138 adantr 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ ( ( F ` i ) ` x ) e. RR ) -> ( G ` x ) e. CC )
140 recn 
 |-  ( ( ( F ` i ) ` x ) e. RR -> ( ( F ` i ) ` x ) e. CC )
141 140 adantl 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ ( ( F ` i ) ` x ) e. RR ) -> ( ( F ` i ) ` x ) e. CC )
142 139 141 abssubd 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ ( ( F ` i ) ` x ) e. RR ) -> ( abs ` ( ( G ` x ) - ( ( F ` i ) ` x ) ) ) = ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) )
143 142 adantrr 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( abs ` ( ( G ` x ) - ( ( F ` i ) ` x ) ) ) = ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) )
144 simprr 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) )
145 143 144 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( abs ` ( ( G ` x ) - ( ( F ` i ) ` x ) ) ) < ( y / 2 ) )
146 145 adantlr 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( abs ` ( ( G ` x ) - ( ( F ` i ) ` x ) ) ) < ( y / 2 ) )
147 131 134 136 137 146 lelttrd 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( ( G ` x ) - ( ( F ` i ) ` x ) ) < ( y / 2 ) )
148 35 adantr 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( G ` x ) e. RR )
149 simprl 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( ( F ` i ) ` x ) e. RR )
150 148 149 136 ltsubadd2d 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( ( ( G ` x ) - ( ( F ` i ) ` x ) ) < ( y / 2 ) <-> ( G ` x ) < ( ( ( F ` i ) ` x ) + ( y / 2 ) ) ) )
151 147 150 mpbid 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) ) -> ( G ` x ) < ( ( ( F ` i ) ` x ) + ( y / 2 ) ) )
152 151 ex 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> ( ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) -> ( G ` x ) < ( ( ( F ` i ) ` x ) + ( y / 2 ) ) ) )
153 152 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ m e. Z ) /\ i e. ( ZZ>= ` m ) ) -> ( ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) -> ( G ` x ) < ( ( ( F ` i ) ` x ) + ( y / 2 ) ) ) )
154 153 ralimdva 
 |-  ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ m e. Z ) -> ( A. i e. ( ZZ>= ` m ) ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) -> A. i e. ( ZZ>= ` m ) ( G ` x ) < ( ( ( F ` i ) ` x ) + ( y / 2 ) ) ) )
155 154 ex 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> ( m e. Z -> ( A. i e. ( ZZ>= ` m ) ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) -> A. i e. ( ZZ>= ` m ) ( G ` x ) < ( ( ( F ` i ) ` x ) + ( y / 2 ) ) ) ) )
156 41 155 reximdai 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> ( E. m e. Z A. i e. ( ZZ>= ` m ) ( ( ( F ` i ) ` x ) e. RR /\ ( abs ` ( ( ( F ` i ) ` x ) - ( G ` x ) ) ) < ( y / 2 ) ) -> E. m e. Z A. i e. ( ZZ>= ` m ) ( G ` x ) < ( ( ( F ` i ) ` x ) + ( y / 2 ) ) ) )
157 127 156 mpd 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> E. m e. Z A. i e. ( ZZ>= ` m ) ( G ` x ) < ( ( ( F ` i ) ` x ) + ( y / 2 ) ) )
158 115 dmeqd 
 |-  ( i = m -> dom ( F ` i ) = dom ( F ` m ) )
159 158 eleq2d 
 |-  ( i = m -> ( x e. dom ( F ` i ) <-> x e. dom ( F ` m ) ) )
160 116 breq1d 
 |-  ( i = m -> ( ( ( F ` i ) ` x ) < ( A + ( y / 2 ) ) <-> ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) )
161 159 160 anbi12d 
 |-  ( i = m -> ( ( x e. dom ( F ` i ) /\ ( ( F ` i ) ` x ) < ( A + ( y / 2 ) ) ) <-> ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) )
162 116 oveq1d 
 |-  ( i = m -> ( ( ( F ` i ) ` x ) + ( y / 2 ) ) = ( ( ( F ` m ) ` x ) + ( y / 2 ) ) )
163 162 breq2d 
 |-  ( i = m -> ( ( G ` x ) < ( ( ( F ` i ) ` x ) + ( y / 2 ) ) <-> ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) ) )
164 41 2 87 157 161 163 rexanuz3 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> E. m e. Z ( ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) ) )
165 df-3an 
 |-  ( ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) ) <-> ( ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) ) )
166 3ancomb 
 |-  ( ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) ) <-> ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) )
167 165 166 bitr3i 
 |-  ( ( ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) ) <-> ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) )
168 167 rexbii 
 |-  ( E. m e. Z ( ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) ) <-> E. m e. Z ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) )
169 164 168 sylib 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> E. m e. Z ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) )
170 35 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( G ` x ) e. RR )
171 22 3adant3 
 |-  ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> ( F ` m ) : dom ( F ` m ) --> RR )
172 simp3 
 |-  ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> x e. dom ( F ` m ) )
173 171 172 ffvelcdmd 
 |-  ( ( ph /\ m e. Z /\ x e. dom ( F ` m ) ) -> ( ( F ` m ) ` x ) e. RR )
174 173 ad4ant134 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ m e. Z ) /\ x e. dom ( F ` m ) ) -> ( ( F ` m ) ` x ) e. RR )
175 simpllr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ m e. Z ) /\ x e. dom ( F ` m ) ) -> y e. RR+ )
176 175 135 syl 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ m e. Z ) /\ x e. dom ( F ` m ) ) -> ( y / 2 ) e. RR )
177 174 176 readdcld 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ m e. Z ) /\ x e. dom ( F ` m ) ) -> ( ( ( F ` m ) ` x ) + ( y / 2 ) ) e. RR )
178 177 adantl3r 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ m e. Z ) /\ x e. dom ( F ` m ) ) -> ( ( ( F ` m ) ` x ) + ( y / 2 ) ) e. RR )
179 178 3ad2antr1 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( ( ( F ` m ) ` x ) + ( y / 2 ) ) e. RR )
180 rehalfcl 
 |-  ( y e. RR -> ( y / 2 ) e. RR )
181 38 180 syl 
 |-  ( ( ph /\ y e. RR+ ) -> ( y / 2 ) e. RR )
182 36 181 jca 
 |-  ( ( ph /\ y e. RR+ ) -> ( A e. RR /\ ( y / 2 ) e. RR ) )
183 readdcl 
 |-  ( ( A e. RR /\ ( y / 2 ) e. RR ) -> ( A + ( y / 2 ) ) e. RR )
184 182 183 syl 
 |-  ( ( ph /\ y e. RR+ ) -> ( A + ( y / 2 ) ) e. RR )
185 184 181 readdcld 
 |-  ( ( ph /\ y e. RR+ ) -> ( ( A + ( y / 2 ) ) + ( y / 2 ) ) e. RR )
186 185 ad5ant13 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( ( A + ( y / 2 ) ) + ( y / 2 ) ) e. RR )
187 simpr2 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) )
188 174 adantrr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( ( F ` m ) ` x ) e. RR )
189 184 ad2antrr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( A + ( y / 2 ) ) e. RR )
190 176 adantrr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( y / 2 ) e. RR )
191 simprr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) )
192 188 189 190 191 ltadd1dd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( ( ( F ` m ) ` x ) + ( y / 2 ) ) < ( ( A + ( y / 2 ) ) + ( y / 2 ) ) )
193 192 adantl3r 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( ( ( F ` m ) ` x ) + ( y / 2 ) ) < ( ( A + ( y / 2 ) ) + ( y / 2 ) ) )
194 193 3adantr2 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( ( ( F ` m ) ` x ) + ( y / 2 ) ) < ( ( A + ( y / 2 ) ) + ( y / 2 ) ) )
195 170 179 186 187 194 lttrd 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( G ` x ) < ( ( A + ( y / 2 ) ) + ( y / 2 ) ) )
196 36 recnd 
 |-  ( ( ph /\ y e. RR+ ) -> A e. CC )
197 181 recnd 
 |-  ( ( ph /\ y e. RR+ ) -> ( y / 2 ) e. CC )
198 196 197 197 addassd 
 |-  ( ( ph /\ y e. RR+ ) -> ( ( A + ( y / 2 ) ) + ( y / 2 ) ) = ( A + ( ( y / 2 ) + ( y / 2 ) ) ) )
199 37 recnd 
 |-  ( y e. RR+ -> y e. CC )
200 2halves 
 |-  ( y e. CC -> ( ( y / 2 ) + ( y / 2 ) ) = y )
201 199 200 syl 
 |-  ( y e. RR+ -> ( ( y / 2 ) + ( y / 2 ) ) = y )
202 201 oveq2d 
 |-  ( y e. RR+ -> ( A + ( ( y / 2 ) + ( y / 2 ) ) ) = ( A + y ) )
203 202 adantl 
 |-  ( ( ph /\ y e. RR+ ) -> ( A + ( ( y / 2 ) + ( y / 2 ) ) ) = ( A + y ) )
204 198 203 eqtrd 
 |-  ( ( ph /\ y e. RR+ ) -> ( ( A + ( y / 2 ) ) + ( y / 2 ) ) = ( A + y ) )
205 204 ad5ant13 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( ( A + ( y / 2 ) ) + ( y / 2 ) ) = ( A + y ) )
206 195 205 breqtrd 
 |-  ( ( ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) /\ m e. Z ) /\ ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) ) -> ( G ` x ) < ( A + y ) )
207 206 rexlimdva2 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> ( E. m e. Z ( x e. dom ( F ` m ) /\ ( G ` x ) < ( ( ( F ` m ) ` x ) + ( y / 2 ) ) /\ ( ( F ` m ) ` x ) < ( A + ( y / 2 ) ) ) -> ( G ` x ) < ( A + y ) ) )
208 169 207 mpd 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> ( G ` x ) < ( A + y ) )
209 35 40 208 ltled 
 |-  ( ( ( ph /\ x e. ( D i^i I ) ) /\ y e. RR+ ) -> ( G ` x ) <_ ( A + y ) )
210 209 ralrimiva 
 |-  ( ( ph /\ x e. ( D i^i I ) ) -> A. y e. RR+ ( G ` x ) <_ ( A + y ) )
211 alrple 
 |-  ( ( ( G ` x ) e. RR /\ A e. RR ) -> ( ( G ` x ) <_ A <-> A. y e. RR+ ( G ` x ) <_ ( A + y ) ) )
212 34 49 211 syl2anc 
 |-  ( ( ph /\ x e. ( D i^i I ) ) -> ( ( G ` x ) <_ A <-> A. y e. RR+ ( G ` x ) <_ ( A + y ) ) )
213 210 212 mpbird 
 |-  ( ( ph /\ x e. ( D i^i I ) ) -> ( G ` x ) <_ A )
214 13 213 ssrabdv 
 |-  ( ph -> ( D i^i I ) C_ { x e. D | ( G ` x ) <_ A } )