Metamath Proof Explorer


Theorem fzsn

Description: A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion fzsn ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )

Proof

Step Hyp Ref Expression
1 elfz1eq ( 𝑘 ∈ ( 𝑀 ... 𝑀 ) → 𝑘 = 𝑀 )
2 elfz3 ( 𝑀 ∈ ℤ → 𝑀 ∈ ( 𝑀 ... 𝑀 ) )
3 eleq1 ( 𝑘 = 𝑀 → ( 𝑘 ∈ ( 𝑀 ... 𝑀 ) ↔ 𝑀 ∈ ( 𝑀 ... 𝑀 ) ) )
4 2 3 syl5ibrcom ( 𝑀 ∈ ℤ → ( 𝑘 = 𝑀𝑘 ∈ ( 𝑀 ... 𝑀 ) ) )
5 1 4 impbid2 ( 𝑀 ∈ ℤ → ( 𝑘 ∈ ( 𝑀 ... 𝑀 ) ↔ 𝑘 = 𝑀 ) )
6 velsn ( 𝑘 ∈ { 𝑀 } ↔ 𝑘 = 𝑀 )
7 5 6 bitr4di ( 𝑀 ∈ ℤ → ( 𝑘 ∈ ( 𝑀 ... 𝑀 ) ↔ 𝑘 ∈ { 𝑀 } ) )
8 7 eqrdv ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )