Metamath Proof Explorer

Theorem allbutfi

Description: For all but finitely many. Some authors say "cofinitely many". Some authors say "ultimately". Compare with eliuniin and eliuniin2 (here, the precondition can be dropped; see eliuniincex ). (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses allbutfi.z 
|- Z = ( ZZ>= ` M )
allbutfi.a 
|- A = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) B
Assertion allbutfi 
|- ( X e. A <-> E. n e. Z A. m e. ( ZZ>= ` n ) X e. B )

Proof

Step Hyp Ref Expression
1 allbutfi.z 
 |-  Z = ( ZZ>= ` M )
2 allbutfi.a 
 |-  A = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) B
3 2 eleq2i 
 |-  ( X e. A <-> X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) B )
4 3 biimpi 
 |-  ( X e. A -> X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) B )
5 eliun 
 |-  ( X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) B <-> E. n e. Z X e. |^|_ m e. ( ZZ>= ` n ) B )
6 4 5 sylib 
 |-  ( X e. A -> E. n e. Z X e. |^|_ m e. ( ZZ>= ` n ) B )
7 nfcv 
 |-  F/_ n X
8 nfiu1 
 |-  F/_ n U_ n e. Z |^|_ m e. ( ZZ>= ` n ) B
9 2 8 nfcxfr 
 |-  F/_ n A
10 7 9 nfel 
 |-  F/ n X e. A
11 eliin 
 |-  ( X e. A -> ( X e. |^|_ m e. ( ZZ>= ` n ) B <-> A. m e. ( ZZ>= ` n ) X e. B ) )
12 11 biimpd 
 |-  ( X e. A -> ( X e. |^|_ m e. ( ZZ>= ` n ) B -> A. m e. ( ZZ>= ` n ) X e. B ) )
13 12 a1d 
 |-  ( X e. A -> ( n e. Z -> ( X e. |^|_ m e. ( ZZ>= ` n ) B -> A. m e. ( ZZ>= ` n ) X e. B ) ) )
14 10 13 reximdai 
 |-  ( X e. A -> ( E. n e. Z X e. |^|_ m e. ( ZZ>= ` n ) B -> E. n e. Z A. m e. ( ZZ>= ` n ) X e. B ) )
15 6 14 mpd 
 |-  ( X e. A -> E. n e. Z A. m e. ( ZZ>= ` n ) X e. B )
16 simpr 
 |-  ( ( n e. Z /\ A. m e. ( ZZ>= ` n ) X e. B ) -> A. m e. ( ZZ>= ` n ) X e. B )
17 1 eleq2i 
 |-  ( n e. Z <-> n e. ( ZZ>= ` M ) )
18 17 biimpi 
 |-  ( n e. Z -> n e. ( ZZ>= ` M ) )
19 eluzelz 
 |-  ( n e. ( ZZ>= ` M ) -> n e. ZZ )
20 uzid 
 |-  ( n e. ZZ -> n e. ( ZZ>= ` n ) )
21 18 19 20 3syl 
 |-  ( n e. Z -> n e. ( ZZ>= ` n ) )
22 21 ne0d 
 |-  ( n e. Z -> ( ZZ>= ` n ) =/= (/) )
23 eliin2 
 |-  ( ( ZZ>= ` n ) =/= (/) -> ( X e. |^|_ m e. ( ZZ>= ` n ) B <-> A. m e. ( ZZ>= ` n ) X e. B ) )
24 22 23 syl 
 |-  ( n e. Z -> ( X e. |^|_ m e. ( ZZ>= ` n ) B <-> A. m e. ( ZZ>= ` n ) X e. B ) )
25 24 adantr 
 |-  ( ( n e. Z /\ A. m e. ( ZZ>= ` n ) X e. B ) -> ( X e. |^|_ m e. ( ZZ>= ` n ) B <-> A. m e. ( ZZ>= ` n ) X e. B ) )
26 16 25 mpbird 
 |-  ( ( n e. Z /\ A. m e. ( ZZ>= ` n ) X e. B ) -> X e. |^|_ m e. ( ZZ>= ` n ) B )
27 26 ex 
 |-  ( n e. Z -> ( A. m e. ( ZZ>= ` n ) X e. B -> X e. |^|_ m e. ( ZZ>= ` n ) B ) )
28 27 reximia 
 |-  ( E. n e. Z A. m e. ( ZZ>= ` n ) X e. B -> E. n e. Z X e. |^|_ m e. ( ZZ>= ` n ) B )
29 28 5 sylibr 
 |-  ( E. n e. Z A. m e. ( ZZ>= ` n ) X e. B -> X e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) B )
30 29 2 eleqtrrdi 
 |-  ( E. n e. Z A. m e. ( ZZ>= ` n ) X e. B -> X e. A )
31 15 30 impbii 
 |-  ( X e. A <-> E. n e. Z A. m e. ( ZZ>= ` n ) X e. B )