Theorem fzo0to2pr

Description: A half-open integer range from 0 to 2 is an unordered pair. (Contributed by Alexander van der Vekens, 4-Dec-2017)

	Ref	Expression
Assertion	fzo0to2pr	|- ( 0 ..^ 2 ) = { 0 , 1 }

Proof

Step	Hyp	Ref	Expression
1		2z	|- 2 e. ZZ
2		fzoval	|- ( 2 e. ZZ -> ( 0 ..^ 2 ) = ( 0 ... ( 2 - 1 ) ) )
3	1 2	ax-mp	|- ( 0 ..^ 2 ) = ( 0 ... ( 2 - 1 ) )
4		2m1e1	|- ( 2 - 1 ) = 1
5		0p1e1	|- ( 0 + 1 ) = 1
6	4 5	eqtr4i	|- ( 2 - 1 ) = ( 0 + 1 )
7	6	oveq2i	|- ( 0 ... ( 2 - 1 ) ) = ( 0 ... ( 0 + 1 ) )
8		0z	|- 0 e. ZZ
9		fzpr	|- ( 0 e. ZZ -> ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
10	5	preq2i	|- { 0 , ( 0 + 1 ) } = { 0 , 1 }
11	9 10	eqtrdi	|- ( 0 e. ZZ -> ( 0 ... ( 0 + 1 ) ) = { 0 , 1 } )
12	8 11	ax-mp	|- ( 0 ... ( 0 + 1 ) ) = { 0 , 1 }
13	3 7 12	3eqtri	|- ( 0 ..^ 2 ) = { 0 , 1 }