This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
allbutfi.a ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵
Assertion allbutfi ( 𝑋 ∈ 𝐴 ↔ ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 allbutfi.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 allbutfi.a ⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵
3 2 eleq2i ⊢ ( 𝑋 ∈ 𝐴 ↔ 𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 )
4 3 biimpi ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 )
5 eliun ⊢ ( 𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 ↔ ∃ 𝑛 ∈ 𝑍 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 )
6 4 5 sylib ⊢ ( 𝑋 ∈ 𝐴 → ∃ 𝑛 ∈ 𝑍 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 )
7 nfcv ⊢ Ⅎ 𝑛 𝑋
8 nfiu1 ⊢ Ⅎ 𝑛 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵
9 2 8 nfcxfr ⊢ Ⅎ 𝑛 𝐴
10 7 9 nfel ⊢ Ⅎ 𝑛 𝑋 ∈ 𝐴
11 eliin ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) )
12 11 biimpd ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) )
13 12 a1d ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑛 ∈ 𝑍 → ( 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) ) )
14 10 13 reximdai ⊢ ( 𝑋 ∈ 𝐴 → ( ∃ 𝑛 ∈ 𝑍 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) )
15 6 14 mpd ⊢ ( 𝑋 ∈ 𝐴 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 )
16 simpr ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 )
17 1 eleq2i ⊢ ( 𝑛 ∈ 𝑍 ↔ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
18 17 biimpi ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
19 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑛 ∈ ℤ )
20 uzid ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
21 18 19 20 3syl ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
22 21 ne0d ⊢ ( 𝑛 ∈ 𝑍 → ( ℤ≥ ‘ 𝑛 ) ≠ ∅ )
23 eliin2 ⊢ ( ( ℤ≥ ‘ 𝑛 ) ≠ ∅ → ( 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) )
24 22 23 syl ⊢ ( 𝑛 ∈ 𝑍 → ( 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) )
25 24 adantr ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) )
26 16 25 mpbird ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 )
27 26 ex ⊢ ( 𝑛 ∈ 𝑍 → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 → 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 ) )
28 27 reximia ⊢ ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 → ∃ 𝑛 ∈ 𝑍 𝑋 ∈ ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 )
29 28 5 sylibr ⊢ ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 → 𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵 )
30 29 2 eleqtrrdi ⊢ ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝐴 )
31 15 30 impbii ⊢ ( 𝑋 ∈ 𝐴 ↔ ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 )