Metamath Proof Explorer

Theorem lmflf

Description: The topological limit relation on functions can be written in terms of the filter limit along the filter generated by the upper integer sets. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses lmflf.1 
|- Z = ( ZZ>= ` M )
lmflf.2 
|- L = ( Z filGen ( ZZ>= " Z ) )
Assertion lmflf 
|- ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( F ( ~~>t ` J ) P <-> P e. ( ( J fLimf L ) ` F ) ) )

Proof

Step Hyp Ref Expression
1 lmflf.1 
 |-  Z = ( ZZ>= ` M )
2 lmflf.2 
 |-  L = ( Z filGen ( ZZ>= " Z ) )
3 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
4 ffn 
 |-  ( ZZ>= : ZZ --> ~P ZZ -> ZZ>= Fn ZZ )
5 3 4 ax-mp 
 |-  ZZ>= Fn ZZ
6 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
7 1 6 eqsstri 
 |-  Z C_ ZZ
8 imaeq2 
 |-  ( y = ( ZZ>= ` j ) -> ( F " y ) = ( F " ( ZZ>= ` j ) ) )
9 8 sseq1d 
 |-  ( y = ( ZZ>= ` j ) -> ( ( F " y ) C_ x <-> ( F " ( ZZ>= ` j ) ) C_ x ) )
10 9 rexima 
 |-  ( ( ZZ>= Fn ZZ /\ Z C_ ZZ ) -> ( E. y e. ( ZZ>= " Z ) ( F " y ) C_ x <-> E. j e. Z ( F " ( ZZ>= ` j ) ) C_ x ) )
11 5 7 10 mp2an 
 |-  ( E. y e. ( ZZ>= " Z ) ( F " y ) C_ x <-> E. j e. Z ( F " ( ZZ>= ` j ) ) C_ x )
12 simpl3 
 |-  ( ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) -> F : Z --> X )
13 12 ffund 
 |-  ( ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) -> Fun F )
14 uzss 
 |-  ( j e. ( ZZ>= ` M ) -> ( ZZ>= ` j ) C_ ( ZZ>= ` M ) )
15 14 1 eleq2s 
 |-  ( j e. Z -> ( ZZ>= ` j ) C_ ( ZZ>= ` M ) )
16 15 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) -> ( ZZ>= ` j ) C_ ( ZZ>= ` M ) )
17 12 fdmd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) -> dom F = Z )
18 17 1 eqtrdi 
 |-  ( ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) -> dom F = ( ZZ>= ` M ) )
19 16 18 sseqtrrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) -> ( ZZ>= ` j ) C_ dom F )
20 funimass4 
 |-  ( ( Fun F /\ ( ZZ>= ` j ) C_ dom F ) -> ( ( F " ( ZZ>= ` j ) ) C_ x <-> A. k e. ( ZZ>= ` j ) ( F ` k ) e. x ) )
21 13 19 20 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ j e. Z ) -> ( ( F " ( ZZ>= ` j ) ) C_ x <-> A. k e. ( ZZ>= ` j ) ( F ` k ) e. x ) )
22 21 rexbidva 
 |-  ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( E. j e. Z ( F " ( ZZ>= ` j ) ) C_ x <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. x ) )
23 11 22 bitr2id 
 |-  ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. x <-> E. y e. ( ZZ>= " Z ) ( F " y ) C_ x ) )
24 23 imbi2d 
 |-  ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( ( P e. x -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. x ) <-> ( P e. x -> E. y e. ( ZZ>= " Z ) ( F " y ) C_ x ) ) )
25 24 ralbidv 
 |-  ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( A. x e. J ( P e. x -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. x ) <-> A. x e. J ( P e. x -> E. y e. ( ZZ>= " Z ) ( F " y ) C_ x ) ) )
26 25 anbi2d 
 |-  ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( ( P e. X /\ A. x e. J ( P e. x -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. x ) ) <-> ( P e. X /\ A. x e. J ( P e. x -> E. y e. ( ZZ>= " Z ) ( F " y ) C_ x ) ) ) )
27 simp1 
 |-  ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> J e. ( TopOn ` X ) )
28 simp2 
 |-  ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> M e. ZZ )
29 simp3 
 |-  ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> F : Z --> X )
30 eqidd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
31 27 1 28 29 30 lmbrf 
 |-  ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( F ( ~~>t ` J ) P <-> ( P e. X /\ A. x e. J ( P e. x -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. x ) ) ) )
32 1 uzfbas 
 |-  ( M e. ZZ -> ( ZZ>= " Z ) e. ( fBas ` Z ) )
33 2 flffbas 
 |-  ( ( J e. ( TopOn ` X ) /\ ( ZZ>= " Z ) e. ( fBas ` Z ) /\ F : Z --> X ) -> ( P e. ( ( J fLimf L ) ` F ) <-> ( P e. X /\ A. x e. J ( P e. x -> E. y e. ( ZZ>= " Z ) ( F " y ) C_ x ) ) ) )
34 32 33 syl3an2 
 |-  ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( P e. ( ( J fLimf L ) ` F ) <-> ( P e. X /\ A. x e. J ( P e. x -> E. y e. ( ZZ>= " Z ) ( F " y ) C_ x ) ) ) )
35 26 31 34 3bitr4d 
 |-  ( ( J e. ( TopOn ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( F ( ~~>t ` J ) P <-> P e. ( ( J fLimf L ) ` F ) ) )