Theorem uzfissfz

Description: For any finite subset of the upper integers, there is a finite set of sequential integers that includes it. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	uzfissfz.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	uzfissfz.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	uzfissfz.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
	uzfissfz.fi	⊢ ( 𝜑 → 𝐴 ∈ Fin )
Assertion	uzfissfz	⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 𝐴 ⊆ ( 𝑀 ... 𝑘 ) )

Proof

Step	Hyp	Ref	Expression
1		uzfissfz.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		uzfissfz.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		uzfissfz.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
4		uzfissfz.fi	⊢ ( 𝜑 → 𝐴 ∈ Fin )
5		uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
6	1 5	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
7	2	a1i	⊢ ( 𝜑 → 𝑍 = ( ℤ≥ ‘ 𝑀 ) )
8	7	eqcomd	⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑀 ) = 𝑍 )
9	6 8	eleqtrd	⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝑀 ∈ 𝑍 )
11		id	⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
12		0ss	⊢ ∅ ⊆ ( 𝑀 ... 𝑀 )
13	12	a1i	⊢ ( 𝐴 = ∅ → ∅ ⊆ ( 𝑀 ... 𝑀 ) )
14	11 13	eqsstrd	⊢ ( 𝐴 = ∅ → 𝐴 ⊆ ( 𝑀 ... 𝑀 ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝐴 ⊆ ( 𝑀 ... 𝑀 ) )
16		oveq2	⊢ ( 𝑘 = 𝑀 → ( 𝑀 ... 𝑘 ) = ( 𝑀 ... 𝑀 ) )
17	16	sseq2d	⊢ ( 𝑘 = 𝑀 → ( 𝐴 ⊆ ( 𝑀 ... 𝑘 ) ↔ 𝐴 ⊆ ( 𝑀 ... 𝑀 ) ) )
18	17	rspcev	⊢ ( ( 𝑀 ∈ 𝑍 ∧ 𝐴 ⊆ ( 𝑀 ... 𝑀 ) ) → ∃ 𝑘 ∈ 𝑍 𝐴 ⊆ ( 𝑀 ... 𝑘 ) )
19	10 15 18	syl2anc	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ∃ 𝑘 ∈ 𝑍 𝐴 ⊆ ( 𝑀 ... 𝑘 ) )
20	3	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ⊆ 𝑍 )
21		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
22	2 21	eqsstri	⊢ 𝑍 ⊆ ℤ
23	22	a1i	⊢ ( 𝜑 → 𝑍 ⊆ ℤ )
24	3 23	sstrd	⊢ ( 𝜑 → 𝐴 ⊆ ℤ )
25	24	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ⊆ ℤ )
26	11	necon3bi	⊢ ( ¬ 𝐴 = ∅ → 𝐴 ≠ ∅ )
27	26	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ≠ ∅ )
28	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ∈ Fin )
29		suprfinzcl	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
30	25 27 28 29	syl3anc	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
31	20 30	sseldd	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ , < ) ∈ 𝑍 )
32	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑀 ∈ ℤ )
33	22 31	sseldi	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ , < ) ∈ ℤ )
34	33	adantr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → sup ( 𝐴 , ℝ , < ) ∈ ℤ )
35	25	sselda	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ℤ )
36	3	sselda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ 𝑍 )
37	2	a1i	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑍 = ( ℤ≥ ‘ 𝑀 ) )
38	36 37	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
39		eluzle	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑗 )
40	38 39	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑀 ≤ 𝑗 )
41	40	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑀 ≤ 𝑗 )
42		zssre	⊢ ℤ ⊆ ℝ
43	24 42	sstrdi	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
44	43	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝐴 ⊆ ℝ )
45	27	adantr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝐴 ≠ ∅ )
46		fimaxre2	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
47	43 4 46	syl2anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
48	47	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
49		simpr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ 𝐴 )
50		suprub	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ≤ sup ( 𝐴 , ℝ , < ) )
51	44 45 48 49 50	syl31anc	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ≤ sup ( 𝐴 , ℝ , < ) )
52	32 34 35 41 51	elfzd	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
53	52	ralrimiva	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ∀ 𝑗 ∈ 𝐴 𝑗 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
54		dfss3	⊢ ( 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ↔ ∀ 𝑗 ∈ 𝐴 𝑗 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
55	53 54	sylibr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
56		oveq2	⊢ ( 𝑘 = sup ( 𝐴 , ℝ , < ) → ( 𝑀 ... 𝑘 ) = ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
57	56	sseq2d	⊢ ( 𝑘 = sup ( 𝐴 , ℝ , < ) → ( 𝐴 ⊆ ( 𝑀 ... 𝑘 ) ↔ 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ) )
58	57	rspcev	⊢ ( ( sup ( 𝐴 , ℝ , < ) ∈ 𝑍 ∧ 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ) → ∃ 𝑘 ∈ 𝑍 𝐴 ⊆ ( 𝑀 ... 𝑘 ) )
59	31 55 58	syl2anc	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑘 ∈ 𝑍 𝐴 ⊆ ( 𝑀 ... 𝑘 ) )
60	19 59	pm2.61dan	⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 𝐴 ⊆ ( 𝑀 ... 𝑘 ) )