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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	allbutfiinf.a	⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵
	allbutfiinf.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	allbutfiinf.n	⊢ 𝑁 = inf ( { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } , ℝ , < )
Assertion	allbutfiinf	⊢ ( 𝜑 → ( 𝑁 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		allbutfiinf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		allbutfiinf.a	⊢ 𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝐵
3		allbutfiinf.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4		allbutfiinf.n	⊢ 𝑁 = inf ( { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } , ℝ , < )
5		ssrab2	⊢ { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ⊆ 𝑍
6	4	a1i	⊢ ( 𝜑 → 𝑁 = inf ( { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } , ℝ , < ) )
7	5 1	sseqtri	⊢ { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ⊆ ( ℤ≥ ‘ 𝑀 )
8	7	a1i	⊢ ( 𝜑 → { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ⊆ ( ℤ≥ ‘ 𝑀 ) )
9	1 2	allbutfi	⊢ ( 𝑋 ∈ 𝐴 ↔ ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 )
10	3 9	sylib	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 )
11		nfrab1	⊢ Ⅎ 𝑛 { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 }
12		nfcv	⊢ Ⅎ 𝑛 ∅
13	11 12	nfne	⊢ Ⅎ 𝑛 { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ≠ ∅
14		rabid	⊢ ( 𝑛 ∈ { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ↔ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) )
15	14	bicomi	⊢ ( ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) ↔ 𝑛 ∈ { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } )
16	15	biimpi	⊢ ( ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) → 𝑛 ∈ { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } )
17	16	ne0d	⊢ ( ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ) → { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ≠ ∅ )
18	17	ex	⊢ ( 𝑛 ∈ 𝑍 → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 → { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ≠ ∅ ) )
19	13 18	rexlimi	⊢ ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 → { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ≠ ∅ )
20	19	a1i	⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 → { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ≠ ∅ ) )
21	10 20	mpd	⊢ ( 𝜑 → { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ≠ ∅ )
22		infssuzcl	⊢ ( ( { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ≠ ∅ ) → inf ( { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } , ℝ , < ) ∈ { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } )
23	8 21 22	syl2anc	⊢ ( 𝜑 → inf ( { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } , ℝ , < ) ∈ { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } )
24	6 23	eqeltrd	⊢ ( 𝜑 → 𝑁 ∈ { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } )
25	5 24	sselid	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
26		nfcv	⊢ Ⅎ 𝑛 ℝ
27		nfcv	⊢ Ⅎ 𝑛 <
28	11 26 27	nfinf	⊢ Ⅎ 𝑛 inf ( { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } , ℝ , < )
29	4 28	nfcxfr	⊢ Ⅎ 𝑛 𝑁
30		nfcv	⊢ Ⅎ 𝑛 𝑍
31		nfcv	⊢ Ⅎ 𝑛 ℤ≥
32	31 29	nffv	⊢ Ⅎ 𝑛 ( ℤ≥ ‘ 𝑁 )
33		nfv	⊢ Ⅎ 𝑛 𝑋 ∈ 𝐵
34	32 33	nfralw	⊢ Ⅎ 𝑛 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ 𝐵
35		nfcv	⊢ Ⅎ 𝑚 ( ℤ≥ ‘ 𝑛 )
36		nfcv	⊢ Ⅎ 𝑚 ℤ≥
37		nfra1	⊢ Ⅎ 𝑚 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵
38		nfcv	⊢ Ⅎ 𝑚 𝑍
39	37 38	nfrabw	⊢ Ⅎ 𝑚 { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 }
40		nfcv	⊢ Ⅎ 𝑚 ℝ
41		nfcv	⊢ Ⅎ 𝑚 <
42	39 40 41	nfinf	⊢ Ⅎ 𝑚 inf ( { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } , ℝ , < )
43	4 42	nfcxfr	⊢ Ⅎ 𝑚 𝑁
44	36 43	nffv	⊢ Ⅎ 𝑚 ( ℤ≥ ‘ 𝑁 )
45		fveq2	⊢ ( 𝑛 = 𝑁 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑁 ) )
46	35 44 45	raleqd	⊢ ( 𝑛 = 𝑁 → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ 𝐵 ) )
47	29 30 34 46	elrabf	⊢ ( 𝑁 ∈ { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } ↔ ( 𝑁 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ 𝐵 ) )
48	47	biimpi	⊢ ( 𝑁 ∈ { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } → ( 𝑁 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ 𝐵 ) )
49	48	simprd	⊢ ( 𝑁 ∈ { 𝑛 ∈ 𝑍 ∣ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) 𝑋 ∈ 𝐵 } → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ 𝐵 )
50	24 49	syl	⊢ ( 𝜑 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ 𝐵 )
51	25 50	jca	⊢ ( 𝜑 → ( 𝑁 ∈ 𝑍 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) 𝑋 ∈ 𝐵 ) )