Description: Subset relationship for finite sets of sequential integers. (Contributed by NM, 21-Jul-2005) (Revised by Mario Carneiro, 28-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fzssp1 | ⊢ ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzel2 | ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℤ ) | |
2 | uzid | ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) ) | |
3 | peano2uz | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) | |
4 | fzss2 | ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) ) | |
5 | 1 2 3 4 | 4syl | ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) ) |
6 | id | ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) | |
7 | 5 6 | sseldd | ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) |
8 | 7 | ssriv | ⊢ ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) |