Metamath Proof Explorer

Theorem fnlimfvre2

Description: The limit function of real functions, applied to elements in its domain, evaluates to Real values. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 fnlimfvre2.p 
 |-  F/ m ph
2 fnlimfvre2.m 
 |-  F/_ m F
3 fnlimfvre2.n 
 |-  F/_ x F
4 fnlimfvre2.z 
 |-  Z = ( ZZ>= ` M )
5 fnlimfvre2.f 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
6 fnlimfvre2.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
7 fnlimfvre2.g 
 |-  G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )
8 fnlimfvre2.x 
 |-  ( ph -> X e. D )
9 nfrab1 
 |-  F/_ x { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
10 6 9 nfcxfr 
 |-  F/_ x D
11 nfcv 
 |-  F/_ z D
12 nfcv 
 |-  F/_ z ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) )
13 nfcv 
 |-  F/_ x ~~>
14 nfcv 
 |-  F/_ x Z
15 nfcv 
 |-  F/_ x m
16 3 15 nffv 
 |-  F/_ x ( F ` m )
17 nfcv 
 |-  F/_ x z
18 16 17 nffv 
 |-  F/_ x ( ( F ` m ) ` z )
19 14 18 nfmpt 
 |-  F/_ x ( m e. Z |-> ( ( F ` m ) ` z ) )
20 13 19 nffv 
 |-  F/_ x ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` z ) ) )
21 fveq2 
 |-  ( x = z -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` z ) )
22 21 mpteq2dv 
 |-  ( x = z -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` z ) ) )
23 22 fveq2d 
 |-  ( x = z -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` z ) ) ) )
24 10 11 12 20 23 cbvmptf 
 |-  ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) ) = ( z e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` z ) ) ) )
25 7 24 eqtri 
 |-  G = ( z e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` z ) ) ) )
26 fveq2 
 |-  ( X = z -> ( ( F ` m ) ` X ) = ( ( F ` m ) ` z ) )
27 26 mpteq2dv 
 |-  ( X = z -> ( m e. Z |-> ( ( F ` m ) ` X ) ) = ( m e. Z |-> ( ( F ` m ) ` z ) ) )
28 eqcom 
 |-  ( X = z <-> z = X )
29 28 imbi1i 
 |-  ( ( X = z -> ( m e. Z |-> ( ( F ` m ) ` X ) ) = ( m e. Z |-> ( ( F ` m ) ` z ) ) ) <-> ( z = X -> ( m e. Z |-> ( ( F ` m ) ` X ) ) = ( m e. Z |-> ( ( F ` m ) ` z ) ) ) )
30 eqcom 
 |-  ( ( m e. Z |-> ( ( F ` m ) ` X ) ) = ( m e. Z |-> ( ( F ` m ) ` z ) ) <-> ( m e. Z |-> ( ( F ` m ) ` z ) ) = ( m e. Z |-> ( ( F ` m ) ` X ) ) )
31 30 imbi2i 
 |-  ( ( z = X -> ( m e. Z |-> ( ( F ` m ) ` X ) ) = ( m e. Z |-> ( ( F ` m ) ` z ) ) ) <-> ( z = X -> ( m e. Z |-> ( ( F ` m ) ` z ) ) = ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )
32 29 31 bitri 
 |-  ( ( X = z -> ( m e. Z |-> ( ( F ` m ) ` X ) ) = ( m e. Z |-> ( ( F ` m ) ` z ) ) ) <-> ( z = X -> ( m e. Z |-> ( ( F ` m ) ` z ) ) = ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )
33 27 32 mpbi 
 |-  ( z = X -> ( m e. Z |-> ( ( F ` m ) ` z ) ) = ( m e. Z |-> ( ( F ` m ) ` X ) ) )
34 33 fveq2d 
 |-  ( z = X -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` z ) ) ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )
35 fvexd 
 |-  ( ph -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. _V )
36 25 34 8 35 fvmptd3 
 |-  ( ph -> ( G ` X ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )
37 1 2 3 4 5 6 8 fnlimfvre 
 |-  ( ph -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )
38 36 37 eqeltrd 
 |-  ( ph -> ( G ` X ) e. RR )