Step |
Hyp |
Ref |
Expression |
1 |
|
dfxlim2.k |
|- F/_ k F |
2 |
|
dfxlim2.m |
|- ( ph -> M e. ZZ ) |
3 |
|
dfxlim2.z |
|- Z = ( ZZ>= ` M ) |
4 |
|
dfxlim2.f |
|- ( ph -> F : Z --> RR* ) |
5 |
2 3 4
|
dfxlim2v |
|- ( ph -> ( F ~~>* A <-> ( F ~~> A \/ ( A = -oo /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) \/ ( A = +oo /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) ) ) ) |
6 |
|
biid |
|- ( F ~~> A <-> F ~~> A ) |
7 |
|
breq2 |
|- ( y = x -> ( ( F ` l ) <_ y <-> ( F ` l ) <_ x ) ) |
8 |
7
|
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 ) ) |
9 |
|
fveq2 |
|- ( i = j -> ( ZZ>= ` i ) = ( ZZ>= ` j ) ) |
10 |
9
|
raleqdv |
|- ( i = j -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. l e. ( ZZ>= ` j ) ( F ` l ) <_ x ) ) |
11 |
|
nfcv |
|- F/_ k l |
12 |
1 11
|
nffv |
|- F/_ k ( F ` l ) |
13 |
|
nfcv |
|- F/_ k <_ |
14 |
|
nfcv |
|- F/_ k x |
15 |
12 13 14
|
nfbr |
|- F/ k ( F ` l ) <_ x |
16 |
|
nfv |
|- F/ l ( F ` k ) <_ x |
17 |
|
fveq2 |
|- ( l = k -> ( F ` l ) = ( F ` k ) ) |
18 |
17
|
breq1d |
|- ( l = k -> ( ( F ` l ) <_ x <-> ( F ` k ) <_ x ) ) |
19 |
15 16 18
|
cbvralw |
|- ( A. l e. ( ZZ>= ` j ) ( F ` l ) <_ x <-> A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) |
20 |
10 19
|
syl6bb |
|- ( i = j -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) ) |
21 |
20
|
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 ) |
22 |
8 21
|
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 ) ) |
23 |
22
|
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 ) |
24 |
23
|
anbi2i |
|- ( ( A = -oo /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) <-> ( A = -oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) ) |
25 |
|
breq1 |
|- ( y = x -> ( y <_ ( F ` l ) <-> x <_ ( F ` l ) ) ) |
26 |
25
|
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 ) ) ) |
27 |
9
|
raleqdv |
|- ( i = j -> ( A. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> A. l e. ( ZZ>= ` j ) x <_ ( F ` l ) ) ) |
28 |
14 13 12
|
nfbr |
|- F/ k x <_ ( F ` l ) |
29 |
|
nfv |
|- F/ l x <_ ( F ` k ) |
30 |
17
|
breq2d |
|- ( l = k -> ( x <_ ( F ` l ) <-> x <_ ( F ` k ) ) ) |
31 |
28 29 30
|
cbvralw |
|- ( A. l e. ( ZZ>= ` j ) x <_ ( F ` l ) <-> A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) |
32 |
27 31
|
syl6bb |
|- ( i = j -> ( A. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) ) |
33 |
32
|
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 ) ) |
34 |
26 33
|
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 ) ) ) |
35 |
34
|
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 ) ) |
36 |
35
|
anbi2i |
|- ( ( A = +oo /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) <-> ( A = +oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) ) |
37 |
6 24 36
|
3orbi123i |
|- ( ( F ~~> A \/ ( A = -oo /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) \/ ( A = +oo /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) ) <-> ( F ~~> A \/ ( A = -oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) \/ ( A = +oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) ) ) |
38 |
5 37
|
syl6bb |
|- ( ph -> ( F ~~>* A <-> ( F ~~> A \/ ( A = -oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) \/ ( A = +oo /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) ) ) ) |