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	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) = { k e. ZZ | ( M <_ k /\ k <_ N ) } )

Proof

Step	Hyp	Ref	Expression
1		breq1	|- ( m = M -> ( m <_ k <-> M <_ k ) )
2	1	anbi1d	|- ( m = M -> ( ( m <_ k /\ k <_ n ) <-> ( M <_ k /\ k <_ n ) ) )
3	2	rabbidv	|- ( m = M -> { k e. ZZ | ( m <_ k /\ k <_ n ) } = { k e. ZZ | ( M <_ k /\ k <_ n ) } )
4		breq2	|- ( n = N -> ( k <_ n <-> k <_ N ) )
5	4	anbi2d	|- ( n = N -> ( ( M <_ k /\ k <_ n ) <-> ( M <_ k /\ k <_ N ) ) )
6	5	rabbidv	|- ( n = N -> { k e. ZZ | ( M <_ k /\ k <_ n ) } = { k e. ZZ | ( M <_ k /\ k <_ N ) } )
7		df-fz	|- ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
8		zex	|- ZZ e. _V
9	8	rabex	|- { k e. ZZ | ( M <_ k /\ k <_ N ) } e. _V
10	3 6 7 9	ovmpo	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) = { k e. ZZ | ( M <_ k /\ k <_ N ) } )