df-fz

Description: Define an operation that produces a finite set of sequential integers. Read " M ... N " as "the set of integers from M to N inclusive". See fzval for its value and additional comments. (Contributed by NM, 6-Sep-2005)

		Ref	Expression
	Assertion	df-fz	⊢ ... = ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ { 𝑘 ∈ ℤ ∣ ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfz	⊢ ...
1		vm	⊢ 𝑚
2		cz	⊢ ℤ
3		vn	⊢ 𝑛
4		vk	⊢ 𝑘
5	1	cv	⊢ 𝑚
6		cle	⊢ ≤
7	4	cv	⊢ 𝑘
8	5 7 6	wbr	⊢ 𝑚 ≤ 𝑘
9	3	cv	⊢ 𝑛
10	7 9 6	wbr	⊢ 𝑘 ≤ 𝑛
11	8 10	wa	⊢ ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 )
12	11 4 2	crab	⊢ { 𝑘 ∈ ℤ ∣ ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) }
13	1 3 2 2 12	cmpo	⊢ ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ { 𝑘 ∈ ℤ ∣ ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) } )
14	0 13	wceq	⊢ ... = ( 𝑚 ∈ ℤ , 𝑛 ∈ ℤ ↦ { 𝑘 ∈ ℤ ∣ ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) } )

Metamath Proof Explorer

Definition df-fz

Detailed syntax breakdown