Metamath Proof Explorer


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 ( 𝐴 , ℝ , < ) ) )