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

Metamath Proof Explorer

Theorem fzss2

Description: Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion fzss2 ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑀 ... 𝐾 ) ⊆ ( 𝑀 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝐾 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 1 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝐾 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
3 elfzuz3 ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝐾 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑘 ) )
4 uztrn ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) )
5 3 4 sylan2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝐾 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) )
6 elfzuzb ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) ) )
7 2 5 6 sylanbrc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝐾 ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
8 7 ex ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑘 ∈ ( 𝑀 ... 𝐾 ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) )
9 8 ssrdv ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑀 ... 𝐾 ) ⊆ ( 𝑀 ... 𝑁 ) )