Step |
Hyp |
Ref |
Expression |
1 |
|
xlimmnf.k |
|- F/_ k F |
2 |
|
xlimmnf.m |
|- ( ph -> M e. ZZ ) |
3 |
|
xlimmnf.z |
|- Z = ( ZZ>= ` M ) |
4 |
|
xlimmnf.f |
|- ( ph -> F : Z --> RR* ) |
5 |
2 3 4
|
xlimmnfv |
|- ( ph -> ( F ~~>* -oo <-> A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) ) |
6 |
|
breq2 |
|- ( y = x -> ( ( F ` l ) <_ y <-> ( F ` l ) <_ x ) ) |
7 |
6
|
rexralbidv |
|- ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x ) ) |
8 |
|
fveq2 |
|- ( i = j -> ( ZZ>= ` i ) = ( ZZ>= ` j ) ) |
9 |
8
|
raleqdv |
|- ( i = j -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. l e. ( ZZ>= ` j ) ( F ` l ) <_ x ) ) |
10 |
|
nfcv |
|- F/_ k l |
11 |
1 10
|
nffv |
|- F/_ k ( F ` l ) |
12 |
|
nfcv |
|- F/_ k <_ |
13 |
|
nfcv |
|- F/_ k x |
14 |
11 12 13
|
nfbr |
|- F/ k ( F ` l ) <_ x |
15 |
|
nfv |
|- F/ l ( F ` k ) <_ x |
16 |
|
fveq2 |
|- ( l = k -> ( F ` l ) = ( F ` k ) ) |
17 |
16
|
breq1d |
|- ( l = k -> ( ( F ` l ) <_ x <-> ( F ` k ) <_ x ) ) |
18 |
14 15 17
|
cbvralw |
|- ( A. l e. ( ZZ>= ` j ) ( F ` l ) <_ x <-> A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) |
19 |
9 18
|
syl6bb |
|- ( i = j -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) ) |
20 |
19
|
cbvrexvw |
|- ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) |
21 |
7 20
|
syl6bb |
|- ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) ) |
22 |
21
|
cbvralvw |
|- ( A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) |
23 |
5 22
|
syl6bb |
|- ( ph -> ( F ~~>* -oo <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) ) |