Theorem ssuzfz

Description: A finite subset of the upper integers is a subset of a finite set of sequential integers. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ssuzfz.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	ssuzfz.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
	ssuzfz.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
Assertion	ssuzfz	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssuzfz.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		ssuzfz.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝑍 )
3		ssuzfz.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
4	2	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝑍 )
5	4 1	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
6		eluzel2	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
7	5 6	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑀 ∈ ℤ )
8		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
9	1 8	eqsstri	⊢ 𝑍 ⊆ ℤ
10	9	a1i	⊢ ( 𝜑 → 𝑍 ⊆ ℤ )
11	2 10	sstrd	⊢ ( 𝜑 → 𝐴 ⊆ ℤ )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐴 ⊆ ℤ )
13		ne0i	⊢ ( 𝑘 ∈ 𝐴 → 𝐴 ≠ ∅ )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐴 ≠ ∅ )
15	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐴 ∈ Fin )
16		suprfinzcl	⊢ ( ( 𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
17	12 14 15 16	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
18	12 17	sseldd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → sup ( 𝐴 , ℝ , < ) ∈ ℤ )
19	11	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ℤ )
20		eluzle	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑘 )
21	5 20	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑀 ≤ 𝑘 )
22		zssre	⊢ ℤ ⊆ ℝ
23	22	a1i	⊢ ( 𝜑 → ℤ ⊆ ℝ )
24	11 23	sstrd	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐴 ⊆ ℝ )
26		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
27		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → sup ( 𝐴 , ℝ , < ) = sup ( 𝐴 , ℝ , < ) )
28	25 15 26 27	supfirege	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ≤ sup ( 𝐴 , ℝ , < ) )
29	7 18 19 21 28	elfzd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
30	29	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ) )
31	30	ralrimiv	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
32		dfss3	⊢ ( 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ↔ ∀ 𝑘 ∈ 𝐴 𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
33	31 32	sylibr	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )