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=ℤ≥M
allbutfiinf.a ⊢A=⋃n∈Z⋂m∈ℤ≥nB
allbutfiinf.x ⊢φ→X∈A
allbutfiinf.n ⊢N=supn∈Z|∀m∈ℤ≥nX∈Bℝ<
Assertion allbutfiinf ⊢φ→N∈Z∧∀m∈ℤ≥NX∈B

Proof

Step Hyp Ref Expression
1 allbutfiinf.z ⊢Z=ℤ≥M
2 allbutfiinf.a ⊢A=⋃n∈Z⋂m∈ℤ≥nB
3 allbutfiinf.x ⊢φ→X∈A
4 allbutfiinf.n ⊢N=supn∈Z|∀m∈ℤ≥nX∈Bℝ<
5 ssrab2 ⊢n∈Z|∀m∈ℤ≥nX∈B⊆Z
6 4 a1i ⊢φ→N=supn∈Z|∀m∈ℤ≥nX∈Bℝ<
7 5 1 sseqtri ⊢n∈Z|∀m∈ℤ≥nX∈B⊆ℤ≥M
8 7 a1i ⊢φ→n∈Z|∀m∈ℤ≥nX∈B⊆ℤ≥M
9 1 2 allbutfi ⊢X∈A↔∃n∈Z∀m∈ℤ≥nX∈B
10 3 9 sylib ⊢φ→∃n∈Z∀m∈ℤ≥nX∈B
11 nfrab1 ⊢Ⅎ_nn∈Z|∀m∈ℤ≥nX∈B
12 nfcv ⊢Ⅎ_n∅
13 11 12 nfne ⊢Ⅎnn∈Z|∀m∈ℤ≥nX∈B≠∅
14 rabid ⊢n∈n∈Z|∀m∈ℤ≥nX∈B↔n∈Z∧∀m∈ℤ≥nX∈B
15 14 bicomi ⊢n∈Z∧∀m∈ℤ≥nX∈B↔n∈n∈Z|∀m∈ℤ≥nX∈B
16 15 biimpi ⊢n∈Z∧∀m∈ℤ≥nX∈B→n∈n∈Z|∀m∈ℤ≥nX∈B
17 16 ne0d ⊢n∈Z∧∀m∈ℤ≥nX∈B→n∈Z|∀m∈ℤ≥nX∈B≠∅
18 17 ex ⊢n∈Z→∀m∈ℤ≥nX∈B→n∈Z|∀m∈ℤ≥nX∈B≠∅
19 13 18 rexlimi ⊢∃n∈Z∀m∈ℤ≥nX∈B→n∈Z|∀m∈ℤ≥nX∈B≠∅
20 19 a1i ⊢φ→∃n∈Z∀m∈ℤ≥nX∈B→n∈Z|∀m∈ℤ≥nX∈B≠∅
21 10 20 mpd ⊢φ→n∈Z|∀m∈ℤ≥nX∈B≠∅
22 infssuzcl ⊢n∈Z|∀m∈ℤ≥nX∈B⊆ℤ≥M∧n∈Z|∀m∈ℤ≥nX∈B≠∅→supn∈Z|∀m∈ℤ≥nX∈Bℝ<∈n∈Z|∀m∈ℤ≥nX∈B
23 8 21 22 syl2anc ⊢φ→supn∈Z|∀m∈ℤ≥nX∈Bℝ<∈n∈Z|∀m∈ℤ≥nX∈B
24 6 23 eqeltrd ⊢φ→N∈n∈Z|∀m∈ℤ≥nX∈B
25 5 24 sselid ⊢φ→N∈Z
26 nfcv ⊢Ⅎ_nℝ
27 nfcv ⊢Ⅎ_n<
28 11 26 27 nfinf ⊢Ⅎ_nsupn∈Z|∀m∈ℤ≥nX∈Bℝ<
29 4 28 nfcxfr ⊢Ⅎ_nN
30 nfcv ⊢Ⅎ_nZ
31 nfcv ⊢Ⅎ_nℤ≥
32 31 29 nffv ⊢Ⅎ_nℤ≥N
33 nfv ⊢ℲnX∈B
34 32 33 nfralw ⊢Ⅎn∀m∈ℤ≥NX∈B
35 nfcv ⊢Ⅎ_mℤ≥n
36 nfcv ⊢Ⅎ_mℤ≥
37 nfra1 ⊢Ⅎm∀m∈ℤ≥nX∈B
38 nfcv ⊢Ⅎ_mZ
39 37 38 nfrabw ⊢Ⅎ_mn∈Z|∀m∈ℤ≥nX∈B
40 nfcv ⊢Ⅎ_mℝ
41 nfcv ⊢Ⅎ_m<
42 39 40 41 nfinf ⊢Ⅎ_msupn∈Z|∀m∈ℤ≥nX∈Bℝ<
43 4 42 nfcxfr ⊢Ⅎ_mN
44 36 43 nffv ⊢Ⅎ_mℤ≥N
45 fveq2 ⊢n=N→ℤ≥n=ℤ≥N
46 35 44 45 raleqd ⊢n=N→∀m∈ℤ≥nX∈B↔∀m∈ℤ≥NX∈B
47 29 30 34 46 elrabf ⊢N∈n∈Z|∀m∈ℤ≥nX∈B↔N∈Z∧∀m∈ℤ≥NX∈B
48 47 biimpi ⊢N∈n∈Z|∀m∈ℤ≥nX∈B→N∈Z∧∀m∈ℤ≥NX∈B
49 48 simprd ⊢N∈n∈Z|∀m∈ℤ≥nX∈B→∀m∈ℤ≥NX∈B
50 24 49 syl ⊢φ→∀m∈ℤ≥NX∈B
51 25 50 jca ⊢φ→N∈Z∧∀m∈ℤ≥NX∈B