Theorem fz0tp

Description: An integer range from 0 to 2 is an unordered triple. (Contributed by Alexander van der Vekens, 1-Feb-2018)

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

Proof

Step	Hyp	Ref	Expression
1		2cn	|- 2 e. CC
2	1	addlidi	|- ( 0 + 2 ) = 2
3	2	eqcomi	|- 2 = ( 0 + 2 )
4	3	oveq2i	|- ( 0 ... 2 ) = ( 0 ... ( 0 + 2 ) )
5		0z	|- 0 e. ZZ
6		fztp	|- ( 0 e. ZZ -> ( 0 ... ( 0 + 2 ) ) = { 0 , ( 0 + 1 ) , ( 0 + 2 ) } )
7	5 6	ax-mp	|- ( 0 ... ( 0 + 2 ) ) = { 0 , ( 0 + 1 ) , ( 0 + 2 ) }
8		eqid	|- 0 = 0
9		id	|- ( 0 = 0 -> 0 = 0 )
10		0p1e1	|- ( 0 + 1 ) = 1
11	10	a1i	|- ( 0 = 0 -> ( 0 + 1 ) = 1 )
12	2	a1i	|- ( 0 = 0 -> ( 0 + 2 ) = 2 )
13	9 11 12	tpeq123d	|- ( 0 = 0 -> { 0 , ( 0 + 1 ) , ( 0 + 2 ) } = { 0 , 1 , 2 } )
14	8 13	ax-mp	|- { 0 , ( 0 + 1 ) , ( 0 + 2 ) } = { 0 , 1 , 2 }
15	4 7 14	3eqtri	|- ( 0 ... 2 ) = { 0 , 1 , 2 }