This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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