Theorem fzval

Description: The value of a finite set of sequential integers. E.g., 2 ... 5 means the set { 2 , 3 , 4 , 5 } . A special case of this definition (starting at 1) appears as Definition 11-2.1 of Gleason p. 141, where NN_k means our 1 ... k ; he calls these setssegments of the integers. (Contributed by NM, 6-Sep-2005) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Assertion	fzval	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) = { 𝑘 ∈ ℤ ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) } )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑚 = 𝑀 → ( 𝑚 ≤ 𝑘 ↔ 𝑀 ≤ 𝑘 ) )
2	1	anbi1d	⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ↔ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) )
3	2	rabbidv	⊢ ( 𝑚 = 𝑀 → { 𝑘 ∈ ℤ ∣ ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) } = { 𝑘 ∈ ℤ ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) } )
4		breq2	⊢ ( 𝑛 = 𝑁 → ( 𝑘 ≤ 𝑛 ↔ 𝑘 ≤ 𝑁 ) )
5	4	anbi2d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ↔ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) )
6	5	rabbidv	⊢ ( 𝑛 = 𝑁 → { 𝑘 ∈ ℤ ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) } = { 𝑘 ∈ ℤ ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) } )
7		df-fz	⊢ ... = ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ { 𝑘 ∈ ℤ ∣ ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) } )
8		zex	⊢ ℤ ∈ V
9	8	rabex	⊢ { 𝑘 ∈ ℤ ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) } ∈ V
10	3 6 7 9	ovmpo	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) = { 𝑘 ∈ ℤ ∣ ( 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) } )