Metamath Proof Explorer

Theorem allbutfiinf

Description: Given a "for all but finitely many" condition, the condition holds from N on. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses allbutfiinf.z 
|- Z = ( ZZ>= ` M )
allbutfiinf.a 
|- A = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) B
allbutfiinf.x 
|- ( ph -> X e. A )
allbutfiinf.n 
|- N = inf ( { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } , RR , < )
Assertion allbutfiinf 
|- ( ph -> ( N e. Z /\ A. m e. ( ZZ>= ` N ) X e. B ) )

Proof

Step Hyp Ref Expression
1 allbutfiinf.z 
 |-  Z = ( ZZ>= ` M )
2 allbutfiinf.a 
 |-  A = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) B
3 allbutfiinf.x 
 |-  ( ph -> X e. A )
4 allbutfiinf.n 
 |-  N = inf ( { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } , RR , < )
5 ssrab2 
 |-  { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } C_ Z
6 4 a1i 
 |-  ( ph -> N = inf ( { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } , RR , < ) )
7 5 1 sseqtri 
 |-  { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } C_ ( ZZ>= ` M )
8 7 a1i 
 |-  ( ph -> { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } C_ ( ZZ>= ` M ) )
9 1 2 allbutfi 
 |-  ( X e. A <-> E. n e. Z A. m e. ( ZZ>= ` n ) X e. B )
10 3 9 sylib 
 |-  ( ph -> E. n e. Z A. m e. ( ZZ>= ` n ) X e. B )
11 nfrab1 
 |-  F/_ n { n e. Z | A. m e. ( ZZ>= ` n ) X e. B }
12 nfcv 
 |-  F/_ n (/)
13 11 12 nfne 
 |-  F/ n { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } =/= (/)
14 rabid 
 |-  ( n e. { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } <-> ( n e. Z /\ A. m e. ( ZZ>= ` n ) X e. B ) )
15 14 bicomi 
 |-  ( ( n e. Z /\ A. m e. ( ZZ>= ` n ) X e. B ) <-> n e. { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } )
16 15 biimpi 
 |-  ( ( n e. Z /\ A. m e. ( ZZ>= ` n ) X e. B ) -> n e. { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } )
17 16 ne0d 
 |-  ( ( n e. Z /\ A. m e. ( ZZ>= ` n ) X e. B ) -> { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } =/= (/) )
18 17 ex 
 |-  ( n e. Z -> ( A. m e. ( ZZ>= ` n ) X e. B -> { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } =/= (/) ) )
19 13 18 rexlimi 
 |-  ( E. n e. Z A. m e. ( ZZ>= ` n ) X e. B -> { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } =/= (/) )
20 19 a1i 
 |-  ( ph -> ( E. n e. Z A. m e. ( ZZ>= ` n ) X e. B -> { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } =/= (/) ) )
21 10 20 mpd 
 |-  ( ph -> { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } =/= (/) )
22 infssuzcl 
 |-  ( ( { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } C_ ( ZZ>= ` M ) /\ { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } =/= (/) ) -> inf ( { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } , RR , < ) e. { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } )
23 8 21 22 syl2anc 
 |-  ( ph -> inf ( { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } , RR , < ) e. { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } )
24 6 23 eqeltrd 
 |-  ( ph -> N e. { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } )
25 5 24 sseldi 
 |-  ( ph -> N e. Z )
26 nfcv 
 |-  F/_ n RR
27 nfcv 
 |-  F/_ n <
28 11 26 27 nfinf 
 |-  F/_ n inf ( { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } , RR , < )
29 4 28 nfcxfr 
 |-  F/_ n N
30 nfcv 
 |-  F/_ n Z
31 nfcv 
 |-  F/_ n ZZ>=
32 31 29 nffv 
 |-  F/_ n ( ZZ>= ` N )
33 nfv 
 |-  F/ n X e. B
34 32 33 nfralw 
 |-  F/ n A. m e. ( ZZ>= ` N ) X e. B
35 nfcv 
 |-  F/_ m ( ZZ>= ` n )
36 nfcv 
 |-  F/_ m ZZ>=
37 nfra1 
 |-  F/ m A. m e. ( ZZ>= ` n ) X e. B
38 nfcv 
 |-  F/_ m Z
39 37 38 nfrabw 
 |-  F/_ m { n e. Z | A. m e. ( ZZ>= ` n ) X e. B }
40 nfcv 
 |-  F/_ m RR
41 nfcv 
 |-  F/_ m <
42 39 40 41 nfinf 
 |-  F/_ m inf ( { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } , RR , < )
43 4 42 nfcxfr 
 |-  F/_ m N
44 36 43 nffv 
 |-  F/_ m ( ZZ>= ` N )
45 fveq2 
 |-  ( n = N -> ( ZZ>= ` n ) = ( ZZ>= ` N ) )
46 35 44 45 raleqd 
 |-  ( n = N -> ( A. m e. ( ZZ>= ` n ) X e. B <-> A. m e. ( ZZ>= ` N ) X e. B ) )
47 29 30 34 46 elrabf 
 |-  ( N e. { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } <-> ( N e. Z /\ A. m e. ( ZZ>= ` N ) X e. B ) )
48 47 biimpi 
 |-  ( N e. { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } -> ( N e. Z /\ A. m e. ( ZZ>= ` N ) X e. B ) )
49 48 simprd 
 |-  ( N e. { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } -> A. m e. ( ZZ>= ` N ) X e. B )
50 24 49 syl 
 |-  ( ph -> A. m e. ( ZZ>= ` N ) X e. B )
51 25 50 jca 
 |-  ( ph -> ( N e. Z /\ A. m e. ( ZZ>= ` N ) X e. B ) )