Metamath Proof Explorer

Theorem fnlimfvre

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 fnlimfvre.p 
|- F/ m ph
fnlimfvre.m 
|- F/_ m F
fnlimfvre.n 
|- F/_ x F
fnlimfvre.z 
|- Z = ( ZZ>= ` M )
fnlimfvre.f 
|- ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
fnlimfvre.d 
|- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
fnlimfvre.x 
|- ( ph -> X e. D )
Assertion fnlimfvre 
|- ( ph -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )

Proof

Step Hyp Ref Expression
1 fnlimfvre.p 
 |-  F/ m ph
2 fnlimfvre.m 
 |-  F/_ m F
3 fnlimfvre.n 
 |-  F/_ x F
4 fnlimfvre.z 
 |-  Z = ( ZZ>= ` M )
5 fnlimfvre.f 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
6 fnlimfvre.d 
 |-  D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
7 fnlimfvre.x 
 |-  ( ph -> X e. D )
8 nfcv 
 |-  F/_ x Z
9 nfcv 
 |-  F/_ x ( ZZ>= ` n )
10 nfcv 
 |-  F/_ x m
11 3 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 14 ssrab2f 
 |-  { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
16 6 15 eqsstri 
 |-  D C_ U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
17 16 sseli 
 |-  ( X e. D -> X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
18 eliun 
 |-  ( X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> E. n e. Z X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
19 17 18 sylib 
 |-  ( X e. D -> E. n e. Z X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
20 7 19 syl 
 |-  ( ph -> E. n e. Z X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
21 nfv 
 |-  F/ n ph
22 nfv 
 |-  F/ n ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR
23 nfv 
 |-  F/ m n e. Z
24 nfcv 
 |-  F/_ m X
25 nfii1 
 |-  F/_ m |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
26 24 25 nfel 
 |-  F/ m X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
27 1 23 26 nf3an 
 |-  F/ m ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
28 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
29 4 eleq2i 
 |-  ( n e. Z <-> n e. ( ZZ>= ` M ) )
30 29 biimpi 
 |-  ( n e. Z -> n e. ( ZZ>= ` M ) )
31 28 30 sselid 
 |-  ( n e. Z -> n e. ZZ )
32 31 3ad2ant2 
 |-  ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> n e. ZZ )
33 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
34 4 fvexi 
 |-  Z e. _V
35 34 a1i 
 |-  ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> Z e. _V )
36 4 uztrn2 
 |-  ( ( n e. Z /\ j e. ( ZZ>= ` n ) ) -> j e. Z )
37 36 ssd 
 |-  ( n e. Z -> ( ZZ>= ` n ) C_ Z )
38 37 3ad2ant2 
 |-  ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( ZZ>= ` n ) C_ Z )
39 fvexd 
 |-  ( ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ m e. Z ) -> ( ( F ` m ) ` X ) e. _V )
40 fvexd 
 |-  ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( ZZ>= ` n ) e. _V )
41 ssidd 
 |-  ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` n ) )
42 fvexd 
 |-  ( ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` X ) e. _V )
43 eqidd 
 |-  ( ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` X ) = ( ( F ` m ) ` X ) )
44 27 32 33 35 38 39 40 41 42 43 climfveqmpt 
 |-  ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) = ( ~~> ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) )
45 6 eleq2i 
 |-  ( X e. D <-> X e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } )
46 45 biimpi 
 |-  ( X e. D -> X e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } )
47 nfcv 
 |-  F/_ x X
48 11 47 nffv 
 |-  F/_ x ( ( F ` m ) ` X )
49 8 48 nfmpt 
 |-  F/_ x ( m e. Z |-> ( ( F ` m ) ` X ) )
50 nfcv 
 |-  F/_ x dom ~~>
51 49 50 nfel 
 |-  F/ x ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~>
52 fveq2 
 |-  ( x = X -> ( ( F ` m ) ` x ) = ( ( F ` m ) ` X ) )
53 52 mpteq2dv 
 |-  ( x = X -> ( m e. Z |-> ( ( F ` m ) ` x ) ) = ( m e. Z |-> ( ( F ` m ) ` X ) ) )
54 53 eleq1d 
 |-  ( x = X -> ( ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> <-> ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~> ) )
55 47 14 51 54 elrabf 
 |-  ( X e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } <-> ( X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~> ) )
56 55 biimpi 
 |-  ( X e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } -> ( X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~> ) )
57 56 simprd 
 |-  ( X e. { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> } -> ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~> )
58 46 57 syl 
 |-  ( X e. D -> ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~> )
59 58 adantr 
 |-  ( ( X e. D /\ n e. Z ) -> ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~> )
60 nfmpt1 
 |-  F/_ m ( m e. Z |-> ( ( F ` m ) ` x ) )
61 nfcv 
 |-  F/_ m dom ~~>
62 60 61 nfel 
 |-  F/ m ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~>
63 nfv 
 |-  F/ m j e. Z
64 63 nfci 
 |-  F/_ m Z
65 64 25 nfiun 
 |-  F/_ m U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
66 62 65 nfrabw 
 |-  F/_ m { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }
67 6 66 nfcxfr 
 |-  F/_ m D
68 24 67 nfel 
 |-  F/ m X e. D
69 68 23 nfan 
 |-  F/ m ( X e. D /\ n e. Z )
70 31 adantl 
 |-  ( ( X e. D /\ n e. Z ) -> n e. ZZ )
71 34 a1i 
 |-  ( ( X e. D /\ n e. Z ) -> Z e. _V )
72 37 adantl 
 |-  ( ( X e. D /\ n e. Z ) -> ( ZZ>= ` n ) C_ Z )
73 fvexd 
 |-  ( ( ( X e. D /\ n e. Z ) /\ m e. Z ) -> ( ( F ` m ) ` X ) e. _V )
74 fvexd 
 |-  ( ( X e. D /\ n e. Z ) -> ( ZZ>= ` n ) e. _V )
75 ssidd 
 |-  ( ( X e. D /\ n e. Z ) -> ( ZZ>= ` n ) C_ ( ZZ>= ` n ) )
76 fvexd 
 |-  ( ( ( X e. D /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` X ) e. _V )
77 eqidd 
 |-  ( ( ( X e. D /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` X ) = ( ( F ` m ) ` X ) )
78 69 70 33 71 72 73 74 75 76 77 climeldmeqmpt 
 |-  ( ( X e. D /\ n e. Z ) -> ( ( m e. Z |-> ( ( F ` m ) ` X ) ) e. dom ~~> <-> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) e. dom ~~> ) )
79 59 78 mpbid 
 |-  ( ( X e. D /\ n e. Z ) -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) e. dom ~~> )
80 climdm 
 |-  ( ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) e. dom ~~> <-> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ~~> ( ~~> ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) )
81 79 80 sylib 
 |-  ( ( X e. D /\ n e. Z ) -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ~~> ( ~~> ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) )
82 7 81 sylan 
 |-  ( ( ph /\ n e. Z ) -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ~~> ( ~~> ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) )
83 82 3adant3 
 |-  ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ~~> ( ~~> ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) )
84 simpl1 
 |-  ( ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ j e. ( ZZ>= ` n ) ) -> ph )
85 simpl2 
 |-  ( ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ j e. ( ZZ>= ` n ) ) -> n e. Z )
86 nfcv 
 |-  F/_ j dom ( F ` m )
87 nfcv 
 |-  F/_ m j
88 2 87 nffv 
 |-  F/_ m ( F ` j )
89 88 nfdm 
 |-  F/_ m dom ( F ` j )
90 fveq2 
 |-  ( m = j -> ( F ` m ) = ( F ` j ) )
91 90 dmeqd 
 |-  ( m = j -> dom ( F ` m ) = dom ( F ` j ) )
92 86 89 91 cbviin 
 |-  |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = |^|_ j e. ( ZZ>= ` n ) dom ( F ` j )
93 92 eleq2i 
 |-  ( X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> X e. |^|_ j e. ( ZZ>= ` n ) dom ( F ` j ) )
94 93 biimpi 
 |-  ( X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> X e. |^|_ j e. ( ZZ>= ` n ) dom ( F ` j ) )
95 94 adantr 
 |-  ( ( X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ j e. ( ZZ>= ` n ) ) -> X e. |^|_ j e. ( ZZ>= ` n ) dom ( F ` j ) )
96 simpr 
 |-  ( ( X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ j e. ( ZZ>= ` n ) ) -> j e. ( ZZ>= ` n ) )
97 eliinid 
 |-  ( ( X e. |^|_ j e. ( ZZ>= ` n ) dom ( F ` j ) /\ j e. ( ZZ>= ` n ) ) -> X e. dom ( F ` j ) )
98 95 96 97 syl2anc 
 |-  ( ( X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ j e. ( ZZ>= ` n ) ) -> X e. dom ( F ` j ) )
99 98 3ad2antl3 
 |-  ( ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ j e. ( ZZ>= ` n ) ) -> X e. dom ( F ` j ) )
100 simpr 
 |-  ( ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ j e. ( ZZ>= ` n ) ) -> j e. ( ZZ>= ` n ) )
101 id 
 |-  ( j e. ( ZZ>= ` n ) -> j e. ( ZZ>= ` n ) )
102 fvexd 
 |-  ( j e. ( ZZ>= ` n ) -> ( ( F ` j ) ` X ) e. _V )
103 88 24 nffv 
 |-  F/_ m ( ( F ` j ) ` X )
104 90 fveq1d 
 |-  ( m = j -> ( ( F ` m ) ` X ) = ( ( F ` j ) ` X ) )
105 eqid 
 |-  ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) )
106 87 103 104 105 fvmptf 
 |-  ( ( j e. ( ZZ>= ` n ) /\ ( ( F ` j ) ` X ) e. _V ) -> ( ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ` j ) = ( ( F ` j ) ` X ) )
107 101 102 106 syl2anc 
 |-  ( j e. ( ZZ>= ` n ) -> ( ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ` j ) = ( ( F ` j ) ` X ) )
108 107 adantl 
 |-  ( ( ( ph /\ n e. Z /\ X e. dom ( F ` j ) ) /\ j e. ( ZZ>= ` n ) ) -> ( ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ` j ) = ( ( F ` j ) ` X ) )
109 simpll 
 |-  ( ( ( ph /\ n e. Z ) /\ j e. ( ZZ>= ` n ) ) -> ph )
110 36 adantll 
 |-  ( ( ( ph /\ n e. Z ) /\ j e. ( ZZ>= ` n ) ) -> j e. Z )
111 1 63 nfan 
 |-  F/ m ( ph /\ j e. Z )
112 nfcv 
 |-  F/_ m RR
113 88 89 112 nff 
 |-  F/ m ( F ` j ) : dom ( F ` j ) --> RR
114 111 113 nfim 
 |-  F/ m ( ( ph /\ j e. Z ) -> ( F ` j ) : dom ( F ` j ) --> RR )
115 eleq1w 
 |-  ( m = j -> ( m e. Z <-> j e. Z ) )
116 115 anbi2d 
 |-  ( m = j -> ( ( ph /\ m e. Z ) <-> ( ph /\ j e. Z ) ) )
117 90 91 feq12d 
 |-  ( m = j -> ( ( F ` m ) : dom ( F ` m ) --> RR <-> ( F ` j ) : dom ( F ` j ) --> RR ) )
118 116 117 imbi12d 
 |-  ( m = j -> ( ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR ) <-> ( ( ph /\ j e. Z ) -> ( F ` j ) : dom ( F ` j ) --> RR ) ) )
119 114 118 5 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) : dom ( F ` j ) --> RR )
120 109 110 119 syl2anc 
 |-  ( ( ( ph /\ n e. Z ) /\ j e. ( ZZ>= ` n ) ) -> ( F ` j ) : dom ( F ` j ) --> RR )
121 120 3adantl3 
 |-  ( ( ( ph /\ n e. Z /\ X e. dom ( F ` j ) ) /\ j e. ( ZZ>= ` n ) ) -> ( F ` j ) : dom ( F ` j ) --> RR )
122 simpl3 
 |-  ( ( ( ph /\ n e. Z /\ X e. dom ( F ` j ) ) /\ j e. ( ZZ>= ` n ) ) -> X e. dom ( F ` j ) )
123 121 122 ffvelcdmd 
 |-  ( ( ( ph /\ n e. Z /\ X e. dom ( F ` j ) ) /\ j e. ( ZZ>= ` n ) ) -> ( ( F ` j ) ` X ) e. RR )
124 108 123 eqeltrd 
 |-  ( ( ( ph /\ n e. Z /\ X e. dom ( F ` j ) ) /\ j e. ( ZZ>= ` n ) ) -> ( ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ` j ) e. RR )
125 84 85 99 100 124 syl31anc 
 |-  ( ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) /\ j e. ( ZZ>= ` n ) ) -> ( ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ` j ) e. RR )
126 33 32 83 125 climrecl 
 |-  ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( ~~> ` ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` X ) ) ) e. RR )
127 44 126 eqeltrd 
 |-  ( ( ph /\ n e. Z /\ X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) ) -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )
128 127 3exp 
 |-  ( ph -> ( n e. Z -> ( X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR ) ) )
129 21 22 128 rexlimd 
 |-  ( ph -> ( E. n e. Z X e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR ) )
130 20 129 mpd 
 |-  ( ph -> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) e. RR )