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 7 18 19 3jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑀 ∈ ℤ ∧ sup ( 𝐴 , ℝ , < ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) )
21 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑘 )
22 5 21 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑀 ≤ 𝑘 )
23 zssre ⊢ ℤ ⊆ ℝ
24 23 a1i ⊢ ( 𝜑 → ℤ ⊆ ℝ )
25 11 24 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐴 ⊆ ℝ )
27 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
28 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → sup ( 𝐴 , ℝ , < ) = sup ( 𝐴 , ℝ , < ) )
29 26 15 27 28 supfirege ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ≤ sup ( 𝐴 , ℝ , < ) )
30 20 22 29 jca32 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑀 ∈ ℤ ∧ sup ( 𝐴 , ℝ , < ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ sup ( 𝐴 , ℝ , < ) ) ) )
31 elfz2 ⊢ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ sup ( 𝐴 , ℝ , < ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ sup ( 𝐴 , ℝ , < ) ) ) )
32 30 31 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
33 32 ex ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ) )
34 33 ralrimiv ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
35 dfss3 ⊢ ( 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ↔ ∀ 𝑘 ∈ 𝐴 𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
36 34 35 sylibr ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )