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	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )