This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnlimcnv

Description: The sequence of function values converges to the value of the limit function G at any point of its domain D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses fnlimcnv.1 
|- F/_ x F
fnlimcnv.2 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
fnlimcnv.3 
|- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
fnlimcnv.4 
|- ( ph -> X e. D )
Assertion fnlimcnv 
|- ( ph -> ( m e. Z |-> ( ( F ` m ) ` X ) ) ~~> ( G ` X ) )

Proof

Step Hyp Ref Expression
1 fnlimcnv.1 
 |-  F/_ x F
2 fnlimcnv.2 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
3 fnlimcnv.3 
 |-  G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
4 fnlimcnv.4 
 |-  ( ph -> X e. D )
5 fveq2 
 |-  ( y = X -> ( ( F ` m ) ` y ) = ( ( F ` m ) ` X ) )
6 5 mpteq2dv 
 |-  ( y = X -> ( m e. Z |-> ( ( F ` m ) ` y ) ) = ( m e. Z |-> ( ( F ` m ) ` X ) ) )
7 6 eleq1d 
 |-  ( y = X -> ( ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~> <-> ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~> ) )
8 nfcv 
 |-  F/_ x Z
9 nfcv 
 |-  F/_ x ( ZZ>= ` n )
10 nfcv 
 |-  F/_ x m
11 1 10 nffv 
 |-  F/_ x ( F ` m )
12 11 nfdm 
 |-  F/_ x dom ( F ` m )
13 9 12 nfiin 
 |-  F/_ x |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
14 8 13 nfiun 
 |-  F/_ x U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
15 nfcv 
 |-  F/_ y U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
16 nfv 
 |-  F/ y ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~>
17 nfcv 
 |-  F/_ x y
18 11 17 nffv 
 |-  F/_ x ( ( F ` m ) ` y )
19 8 18 nfmpt 
 |-  F/_ x ( m e. Z |-> ( ( F ` m ) ` y ) )
20 nfcv 
 |-  F/_ x dom ~~>
21 19 20 nfel 
 |-  F/ x ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~>
22 fveq2 
 |-  ( x = y -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` y ) )
23 22 mpteq2dv 
 |-  ( x = y -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` y ) ) )
24 23 eleq1d 
 |-  ( x = y -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> <-> ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~> ) )
25 14 15 16 21 24 cbvrabw 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } = { y e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~> }
26 2 25 eqtri 
 |-  D = { y e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` y ) ) e. dom ~~> }
27 7 26 elrab2 
 |-  ( X e. D <-> ( X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~> ) )
28 4 27 sylib 
 |-  ( ph -> ( X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~> ) )
29 28 simprd 
 |-  ( ph -> ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~> )
30 climdm 
 |-  ( ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~> <-> ( m e. Z |-> ( ( F ` m ) ` X ) ) ~~> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )
31 29 30 sylib 
 |-  ( ph -> ( m e. Z |-> ( ( F ` m ) ` X ) ) ~~> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )
32 nfrab1 
 |-  F/_ x { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
33 2 32 nfcxfr 
 |-  F/_ x D
34 33 1 3 4 fnlimfv 
 |-  ( ph -> ( G ` X ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )
35 34 eqcomd 
 |-  ( ph -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) = ( G ` X ) )
36 31 35 breqtrd 
 |-  ( ph -> ( m e. Z |-> ( ( F ` m ) ` X ) ) ~~> ( G ` X ) )