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={\mathbb{Z}}_{\ge M}$$
	allbutfi.a	$$⊢A=\bigcup _{n\in Z}\bigcap _{m\in {\mathbb{Z}}_{\ge n}}B$$
Assertion	allbutfi	$$⊢X\in A\leftrightarrow \exists n\in Z\forall m\in {\mathbb{Z}}_{\ge n}X\in B$$

Proof

Step	Hyp	Ref	Expression
1		allbutfi.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		allbutfi.a	$$⊢A=\bigcup _{n\in Z}\bigcap _{m\in {\mathbb{Z}}_{\ge n}}B$$
3	2	eleq2i	$$⊢X\in A\leftrightarrow X\in \bigcup _{n\in Z}\bigcap _{m\in {\mathbb{Z}}_{\ge n}}B$$
4	3	biimpi	$$⊢X\in A\to X\in \bigcup _{n\in Z}\bigcap _{m\in {\mathbb{Z}}_{\ge n}}B$$
5		eliun	$$⊢X\in \bigcup _{n\in Z}\bigcap _{m\in {\mathbb{Z}}_{\ge n}}B\leftrightarrow \exists n\in ZX\in \bigcap _{m\in {\mathbb{Z}}_{\ge n}}B$$
6	4 5	sylib	$$⊢X\in A\to \exists n\in ZX\in \bigcap _{m\in {\mathbb{Z}}_{\ge n}}B$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}nX$$
8		nfiu1	$$⊢\underset{\_}{Ⅎ}n\bigcup _{n\in Z}\bigcap _{m\in {\mathbb{Z}}_{\ge n}}B$$
9	2 8	nfcxfr	$$⊢\underset{\_}{Ⅎ}nA$$
10	7 9	nfel	$$⊢ℲnX\in A$$
11		eliin	$$⊢X\in A\to \left(X\in \bigcap _{m\in {\mathbb{Z}}_{\ge n}}B\leftrightarrow \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)$$
12	11	biimpd	$$⊢X\in A\to \left(X\in \bigcap _{m\in {\mathbb{Z}}_{\ge n}}B\to \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)$$
13	12	a1d	$$⊢X\in A\to \left(n\in Z\to \left(X\in \bigcap _{m\in {\mathbb{Z}}_{\ge n}}B\to \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)\right)$$
14	10 13	reximdai	$$⊢X\in A\to \left(\exists n\in ZX\in \bigcap _{m\in {\mathbb{Z}}_{\ge n}}B\to \exists n\in Z\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)$$
15	6 14	mpd	$$⊢X\in A\to \exists n\in Z\forall m\in {\mathbb{Z}}_{\ge n}X\in B$$
16		simpr	$$⊢\left(n\in Z\wedge \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)\to \forall m\in {\mathbb{Z}}_{\ge n}X\in B$$
17	1	eleq2i	$$⊢n\in Z\leftrightarrow n\in {\mathbb{Z}}_{\ge M}$$
18	17	biimpi	$$⊢n\in Z\to n\in {\mathbb{Z}}_{\ge M}$$
19		eluzelz	$$⊢n\in {\mathbb{Z}}_{\ge M}\to n\in \mathbb{Z}$$
20		uzid	$$⊢n\in \mathbb{Z}\to n\in {\mathbb{Z}}_{\ge n}$$
21	18 19 20	3syl	$$⊢n\in Z\to n\in {\mathbb{Z}}_{\ge n}$$
22	21	ne0d	$$⊢n\in Z\to {\mathbb{Z}}_{\ge n}\ne \varnothing$$
23		eliin2	$$⊢{\mathbb{Z}}_{\ge n}\ne \varnothing \to \left(X\in \bigcap _{m\in {\mathbb{Z}}_{\ge n}}B\leftrightarrow \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)$$
24	22 23	syl	$$⊢n\in Z\to \left(X\in \bigcap _{m\in {\mathbb{Z}}_{\ge n}}B\leftrightarrow \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)$$
25	24	adantr	$$⊢\left(n\in Z\wedge \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)\to \left(X\in \bigcap _{m\in {\mathbb{Z}}_{\ge n}}B\leftrightarrow \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)$$
26	16 25	mpbird	$$⊢\left(n\in Z\wedge \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)\to X\in \bigcap _{m\in {\mathbb{Z}}_{\ge n}}B$$
27	26	ex	$$⊢n\in Z\to \left(\forall m\in {\mathbb{Z}}_{\ge n}X\in B\to X\in \bigcap _{m\in {\mathbb{Z}}_{\ge n}}B\right)$$
28	27	reximia	$$⊢\exists n\in Z\forall m\in {\mathbb{Z}}_{\ge n}X\in B\to \exists n\in ZX\in \bigcap _{m\in {\mathbb{Z}}_{\ge n}}B$$
29	28 5	sylibr	$$⊢\exists n\in Z\forall m\in {\mathbb{Z}}_{\ge n}X\in B\to X\in \bigcup _{n\in Z}\bigcap _{m\in {\mathbb{Z}}_{\ge n}}B$$
30	29 2	eleqtrrdi	$$⊢\exists n\in Z\forall m\in {\mathbb{Z}}_{\ge n}X\in B\to X\in A$$
31	15 30	impbii	$$⊢X\in A\leftrightarrow \exists n\in Z\forall m\in {\mathbb{Z}}_{\ge n}X\in B$$