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	$⊢ \dots = (m \in ℤ, n \in ℤ ⟼ \{k \in ℤ \| (m \leq k \land k \leq n)\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfz	$class \dots$
1		vm	$setvar m$
2		cz	$class ℤ$
3		vn	$setvar n$
4		vk	$setvar k$
5	1	cv	$setvar m$
6		cle	$class \leq$
7	4	cv	$setvar k$
8	5 7 6	wbr	$wff m \leq k$
9	3	cv	$setvar n$
10	7 9 6	wbr	$wff k \leq n$
11	8 10	wa	$wff (m \leq k \land k \leq n)$
12	11 4 2	crab	$class \{k \in ℤ \| (m \leq k \land k \leq n)\}$
13	1 3 2 2 12	cmpo	$class (m \in ℤ, n \in ℤ ⟼ \{k \in ℤ \| (m \leq k \land k \leq n)\})$
14	0 13	wceq	$wff \dots = (m \in ℤ, n \in ℤ ⟼ \{k \in ℤ \| (m \leq k \land k \leq n)\})$

Metamath Proof Explorer

Definition df-fz

Detailed syntax breakdown