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