Metamath Proof Explorer


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 addid2i
 |-  ( 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 }