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={\mathbb{Z}}_{\ge M}$$
	allbutfiinf.a	$$⊢A=\bigcup _{n\in Z}\bigcap _{m\in {\mathbb{Z}}_{\ge n}}B$$
	allbutfiinf.x	$$⊢\phi \to X\in A$$
	allbutfiinf.n	$$⊢N=inf\left(\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\},ℝ,<\right)$$
Assertion	allbutfiinf	$$⊢\phi \to \left(N\in Z\wedge \forall m\in {\mathbb{Z}}_{\ge N}X\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		allbutfiinf.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		allbutfiinf.a	$$⊢A=\bigcup _{n\in Z}\bigcap _{m\in {\mathbb{Z}}_{\ge n}}B$$
3		allbutfiinf.x	$$⊢\phi \to X\in A$$
4		allbutfiinf.n	$$⊢N=inf\left(\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\},ℝ,<\right)$$
5		ssrab2	$$⊢\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\subseteq Z$$
6	4	a1i	$$⊢\phi \to N=inf\left(\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\},ℝ,<\right)$$
7	5 1	sseqtri	$$⊢\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\subseteq {\mathbb{Z}}_{\ge M}$$
8	7	a1i	$$⊢\phi \to \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\subseteq {\mathbb{Z}}_{\ge M}$$
9	1 2	allbutfi	$$⊢X\in A\leftrightarrow \exists n\in Z\forall m\in {\mathbb{Z}}_{\ge n}X\in B$$
10	3 9	sylib	$$⊢\phi \to \exists n\in Z\forall m\in {\mathbb{Z}}_{\ge n}X\in B$$
11		nfrab1	$$⊢\underset{\_}{Ⅎ}n\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}n\varnothing$$
13	11 12	nfne	$$⊢Ⅎn\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\ne \varnothing$$
14		rabid	$$⊢n\in \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\leftrightarrow \left(n\in Z\wedge \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)$$
15	14	bicomi	$$⊢\left(n\in Z\wedge \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)\leftrightarrow n\in \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}$$
16	15	biimpi	$$⊢\left(n\in Z\wedge \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)\to n\in \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}$$
17	16	ne0d	$$⊢\left(n\in Z\wedge \forall m\in {\mathbb{Z}}_{\ge n}X\in B\right)\to \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\ne \varnothing$$
18	17	ex	$$⊢n\in Z\to \left(\forall m\in {\mathbb{Z}}_{\ge n}X\in B\to \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\ne \varnothing \right)$$
19	13 18	rexlimi	$$⊢\exists n\in Z\forall m\in {\mathbb{Z}}_{\ge n}X\in B\to \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\ne \varnothing$$
20	19	a1i	$$⊢\phi \to \left(\exists n\in Z\forall m\in {\mathbb{Z}}_{\ge n}X\in B\to \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\ne \varnothing \right)$$
21	10 20	mpd	$$⊢\phi \to \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\ne \varnothing$$
22		infssuzcl	$$⊢\left(\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\subseteq {\mathbb{Z}}_{\ge M}\wedge \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\ne \varnothing \right)\to inf\left(\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\},ℝ,<\right)\in \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}$$
23	8 21 22	syl2anc	$$⊢\phi \to inf\left(\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\},ℝ,<\right)\in \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}$$
24	6 23	eqeltrd	$$⊢\phi \to N\in \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}$$
25	5 24	sselid	$$⊢\phi \to N\in Z$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}nℝ$$
27		nfcv	$$⊢\underset{\_}{Ⅎ}n<$$
28	11 26 27	nfinf	$$⊢\underset{\_}{Ⅎ}ninf\left(\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\},ℝ,<\right)$$
29	4 28	nfcxfr	$$⊢\underset{\_}{Ⅎ}nN$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}nZ$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}n{\mathbb{Z}}_{\ge }$$
32	31 29	nffv	$$⊢\underset{\_}{Ⅎ}n{\mathbb{Z}}_{\ge N}$$
33		nfv	$$⊢ℲnX\in B$$
34	32 33	nfralw	$$⊢Ⅎn\forall m\in {\mathbb{Z}}_{\ge N}X\in B$$
35		nfcv	$$⊢\underset{\_}{Ⅎ}m{\mathbb{Z}}_{\ge n}$$
36		nfcv	$$⊢\underset{\_}{Ⅎ}m{\mathbb{Z}}_{\ge }$$
37		nfra1	$$⊢Ⅎm\forall m\in {\mathbb{Z}}_{\ge n}X\in B$$
38		nfcv	$$⊢\underset{\_}{Ⅎ}mZ$$
39	37 38	nfrabw	$$⊢\underset{\_}{Ⅎ}m\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}$$
40		nfcv	$$⊢\underset{\_}{Ⅎ}mℝ$$
41		nfcv	$$⊢\underset{\_}{Ⅎ}m<$$
42	39 40 41	nfinf	$$⊢\underset{\_}{Ⅎ}minf\left(\left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\},ℝ,<\right)$$
43	4 42	nfcxfr	$$⊢\underset{\_}{Ⅎ}mN$$
44	36 43	nffv	$$⊢\underset{\_}{Ⅎ}m{\mathbb{Z}}_{\ge N}$$
45		fveq2	$$⊢n=N\to {\mathbb{Z}}_{\ge n}={\mathbb{Z}}_{\ge N}$$
46	35 44 45	raleqd	$$⊢n=N\to \left(\forall m\in {\mathbb{Z}}_{\ge n}X\in B\leftrightarrow \forall m\in {\mathbb{Z}}_{\ge N}X\in B\right)$$
47	29 30 34 46	elrabf	$$⊢N\in \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\leftrightarrow \left(N\in Z\wedge \forall m\in {\mathbb{Z}}_{\ge N}X\in B\right)$$
48	47	biimpi	$$⊢N\in \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\to \left(N\in Z\wedge \forall m\in {\mathbb{Z}}_{\ge N}X\in B\right)$$
49	48	simprd	$$⊢N\in \left\{n\in Z|\forall m\in {\mathbb{Z}}_{\ge n}X\in B\right\}\to \forall m\in {\mathbb{Z}}_{\ge N}X\in B$$
50	24 49	syl	$$⊢\phi \to \forall m\in {\mathbb{Z}}_{\ge N}X\in B$$
51	25 50	jca	$$⊢\phi \to \left(N\in Z\wedge \forall m\in {\mathbb{Z}}_{\ge N}X\in B\right)$$