Metamath Proof Explorer

Theorem lmff

Description: If F converges, there is some upper integer set on which F is a total function. (Contributed by Mario Carneiro, 31-Dec-2013)

Ref Expression
Hypotheses lmff.1 
|- Z = ( ZZ>= ` M )
lmff.3 
|- ( ph -> J e. ( TopOn ` X ) )
lmff.4 
|- ( ph -> M e. ZZ )
lmff.5 
|- ( ph -> F e. dom ( ~~>t ` J ) )
Assertion lmff 
|- ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X )

Proof

Step Hyp Ref Expression
1 lmff.1 
 |-  Z = ( ZZ>= ` M )
2 lmff.3 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 lmff.4 
 |-  ( ph -> M e. ZZ )
4 lmff.5 
 |-  ( ph -> F e. dom ( ~~>t ` J ) )
5 eldm2g 
 |-  ( F e. dom ( ~~>t ` J ) -> ( F e. dom ( ~~>t ` J ) <-> E. y <. F , y >. e. ( ~~>t ` J ) ) )
6 5 ibi 
 |-  ( F e. dom ( ~~>t ` J ) -> E. y <. F , y >. e. ( ~~>t ` J ) )
7 4 6 syl 
 |-  ( ph -> E. y <. F , y >. e. ( ~~>t ` J ) )
8 df-br 
 |-  ( F ( ~~>t ` J ) y <-> <. F , y >. e. ( ~~>t ` J ) )
9 8 exbii 
 |-  ( E. y F ( ~~>t ` J ) y <-> E. y <. F , y >. e. ( ~~>t ` J ) )
10 7 9 sylibr 
 |-  ( ph -> E. y F ( ~~>t ` J ) y )
11 lmcl 
 |-  ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) y ) -> y e. X )
12 2 11 sylan 
 |-  ( ( ph /\ F ( ~~>t ` J ) y ) -> y e. X )
13 eleq2 
 |-  ( j = X -> ( y e. j <-> y e. X ) )
14 feq3 
 |-  ( j = X -> ( ( F |` x ) : x --> j <-> ( F |` x ) : x --> X ) )
15 14 rexbidv 
 |-  ( j = X -> ( E. x e. ran ZZ>= ( F |` x ) : x --> j <-> E. x e. ran ZZ>= ( F |` x ) : x --> X ) )
16 13 15 imbi12d 
 |-  ( j = X -> ( ( y e. j -> E. x e. ran ZZ>= ( F |` x ) : x --> j ) <-> ( y e. X -> E. x e. ran ZZ>= ( F |` x ) : x --> X ) ) )
17 2 lmbr 
 |-  ( ph -> ( F ( ~~>t ` J ) y <-> ( F e. ( X ^pm CC ) /\ y e. X /\ A. j e. J ( y e. j -> E. x e. ran ZZ>= ( F |` x ) : x --> j ) ) ) )
18 17 biimpa 
 |-  ( ( ph /\ F ( ~~>t ` J ) y ) -> ( F e. ( X ^pm CC ) /\ y e. X /\ A. j e. J ( y e. j -> E. x e. ran ZZ>= ( F |` x ) : x --> j ) ) )
19 18 simp3d 
 |-  ( ( ph /\ F ( ~~>t ` J ) y ) -> A. j e. J ( y e. j -> E. x e. ran ZZ>= ( F |` x ) : x --> j ) )
20 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
21 2 20 syl 
 |-  ( ph -> X e. J )
22 21 adantr 
 |-  ( ( ph /\ F ( ~~>t ` J ) y ) -> X e. J )
23 16 19 22 rspcdva 
 |-  ( ( ph /\ F ( ~~>t ` J ) y ) -> ( y e. X -> E. x e. ran ZZ>= ( F |` x ) : x --> X ) )
24 12 23 mpd 
 |-  ( ( ph /\ F ( ~~>t ` J ) y ) -> E. x e. ran ZZ>= ( F |` x ) : x --> X )
25 10 24 exlimddv 
 |-  ( ph -> E. x e. ran ZZ>= ( F |` x ) : x --> X )
26 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
27 ffn 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> ZZ>= Fn ZZ )
28 reseq2 
 |-  ( x = ( ZZ>= ` j ) -> ( F |` x ) = ( F |` ( ZZ>= ` j ) ) )
29 id 
 |-  ( x = ( ZZ>= ` j ) -> x = ( ZZ>= ` j ) )
30 28 29 feq12d 
 |-  ( x = ( ZZ>= ` j ) -> ( ( F |` x ) : x --> X <-> ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) )
31 30 rexrn 
 |-  ( ZZ>= Fn ZZ -> ( E. x e. ran ZZ>= ( F |` x ) : x --> X <-> E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) )
32 26 27 31 mp2b 
 |-  ( E. x e. ran ZZ>= ( F |` x ) : x --> X <-> E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X )
33 25 32 sylib 
 |-  ( ph -> E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X )
34 1 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z A. x e. ( ZZ>= ` j ) ( x e. dom F /\ ( F ` x ) e. X ) <-> E. j e. ZZ A. x e. ( ZZ>= ` j ) ( x e. dom F /\ ( F ` x ) e. X ) ) )
35 3 34 syl 
 |-  ( ph -> ( E. j e. Z A. x e. ( ZZ>= ` j ) ( x e. dom F /\ ( F ` x ) e. X ) <-> E. j e. ZZ A. x e. ( ZZ>= ` j ) ( x e. dom F /\ ( F ` x ) e. X ) ) )
36 18 simp1d 
 |-  ( ( ph /\ F ( ~~>t ` J ) y ) -> F e. ( X ^pm CC ) )
37 10 36 exlimddv 
 |-  ( ph -> F e. ( X ^pm CC ) )
38 pmfun 
 |-  ( F e. ( X ^pm CC ) -> Fun F )
39 37 38 syl 
 |-  ( ph -> Fun F )
40 ffvresb 
 |-  ( Fun F -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X <-> A. x e. ( ZZ>= ` j ) ( x e. dom F /\ ( F ` x ) e. X ) ) )
41 39 40 syl 
 |-  ( ph -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X <-> A. x e. ( ZZ>= ` j ) ( x e. dom F /\ ( F ` x ) e. X ) ) )
42 41 rexbidv 
 |-  ( ph -> ( E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X <-> E. j e. Z A. x e. ( ZZ>= ` j ) ( x e. dom F /\ ( F ` x ) e. X ) ) )
43 41 rexbidv 
 |-  ( ph -> ( E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X <-> E. j e. ZZ A. x e. ( ZZ>= ` j ) ( x e. dom F /\ ( F ` x ) e. X ) ) )
44 35 42 43 3bitr4d 
 |-  ( ph -> ( E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X <-> E. j e. ZZ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) )
45 33 44 mpbird 
 |-  ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X )