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