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

Metamath Proof Explorer

Theorem fnlimf

Description: The limit function of real functions, is a real-valued function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses fnlimf.p 
|- F/ m ph
fnlimf.m 
|- F/_ m F
fnlimf.n 
|- F/_ x F
fnlimf.z 
|- Z = ( ZZ>= ` M )
fnlimf.f 
|- ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
fnlimf.d 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
fnlimf.g 
|- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
Assertion fnlimf 
|- ( ph -> G : D --> RR )

Proof

Step Hyp Ref Expression
1 fnlimf.p 
 |-  F/ m ph
2 fnlimf.m 
 |-  F/_ m F
3 fnlimf.n 
 |-  F/_ x F
4 fnlimf.z 
 |-  Z = ( ZZ>= ` M )
5 fnlimf.f 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
6 fnlimf.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
7 fnlimf.g 
 |-  G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
8 nfv 
 |-  F/ m z e. D
9 1 8 nfan 
 |-  F/ m ( ph /\ z e. D )
10 5 adantlr 
 |-  ( ( ( ph /\ z e. D ) /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
11 simpr 
 |-  ( ( ph /\ z e. D ) -> z e. D )
12 9 2 3 4 10 6 11 fnlimfvre 
 |-  ( ( ph /\ z e. D ) -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` z ) ) ) e. RR )
13 nfrab1 
 |-  F/_ x { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
14 6 13 nfcxfr 
 |-  F/_ x D
15 nfcv 
 |-  F/_ z D
16 nfcv 
 |-  F/_ z ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) )
17 nfcv 
 |-  F/_ x ~~>
18 nfcv 
 |-  F/_ x Z
19 nfcv 
 |-  F/_ x m
20 3 19 nffv 
 |-  F/_ x ( F ` m )
21 nfcv 
 |-  F/_ x z
22 20 21 nffv 
 |-  F/_ x ( ( F ` m ) ` z )
23 18 22 nfmpt 
 |-  F/_ x ( m e. Z |-> ( ( F ` m ) ` z ) )
24 17 23 nffv 
 |-  F/_ x ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` z ) ) )
25 fveq2 
 |-  ( x = z -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` z ) )
26 25 mpteq2dv 
 |-  ( x = z -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` z ) ) )
27 26 fveq2d 
 |-  ( x = z -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` z ) ) ) )
28 14 15 16 24 27 cbvmptf 
 |-  ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) = ( z e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` z ) ) ) )
29 7 28 eqtri 
 |-  G = ( z e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` z ) ) ) )
30 12 29 fmptd 
 |-  ( ph -> G : D --> RR )