Metamath Proof Explorer

Theorem allbutfifvre

Description: Given a sequence of real-valued functions, and X that belongs to all but finitely many domains, then its function value is ultimately a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses allbutfifvre.1 
|- F/ m ph
allbutfifvre.2 
|- Z = ( ZZ>= ` M )
allbutfifvre.3 
|- ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
allbutfifvre.4 
|- D = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
allbutfifvre.5 
|- ( ph -> X e. D )
Assertion allbutfifvre 
|- ( ph -> E. n e. Z A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) e. RR )

Proof

Step Hyp Ref Expression
1 allbutfifvre.1 
 |-  F/ m ph
2 allbutfifvre.2 
 |-  Z = ( ZZ>= ` M )
3 allbutfifvre.3 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) : dom ( F ` m ) --> RR )
4 allbutfifvre.4 
 |-  D = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
5 allbutfifvre.5 
 |-  ( ph -> X e. D )
6 5 4 eleqtrdi 
 |-  ( ph -> X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) )
7 eqid 
 |-  U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m )
8 2 7 allbutfi 
 |-  ( X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) <-> E. n e. Z A. m e. ( ZZ>= ` n ) X e. dom ( F ` m ) )
9 6 8 sylib 
 |-  ( ph -> E. n e. Z A. m e. ( ZZ>= ` n ) X e. dom ( F ` m ) )
10 nfv 
 |-  F/ m n e. Z
11 1 10 nfan 
 |-  F/ m ( ph /\ n e. Z )
12 simpll 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ph )
13 2 uztrn2 
 |-  ( ( n e. Z /\ j e. ( ZZ>= ` n ) ) -> j e. Z )
14 13 ssd 
 |-  ( n e. Z -> ( ZZ>= ` n ) C_ Z )
15 14 sselda 
 |-  ( ( n e. Z /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
16 15 adantll 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
17 3 ffvelrnda 
 |-  ( ( ( ph /\ m e. Z ) /\ X e. dom ( F ` m ) ) -> ( ( F ` m ) ` X ) e. RR )
18 17 ex 
 |-  ( ( ph /\ m e. Z ) -> ( X e. dom ( F ` m ) -> ( ( F ` m ) ` X ) e. RR ) )
19 12 16 18 syl2anc 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ( X e. dom ( F ` m ) -> ( ( F ` m ) ` X ) e. RR ) )
20 11 19 ralimdaa 
 |-  ( ( ph /\ n e. Z ) -> ( A. m e. ( ZZ>= ` n ) X e. dom ( F ` m ) -> A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) e. RR ) )
21 20 reximdva 
 |-  ( ph -> ( E. n e. Z A. m e. ( ZZ>= ` n ) X e. dom ( F ` m ) -> E. n e. Z A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) e. RR ) )
22 9 21 mpd 
 |-  ( ph -> E. n e. Z A. m e. ( ZZ>= ` n ) ( ( F ` m ) ` X ) e. RR )