Metamath Proof Explorer


Theorem fzo12sn

Description: A 1-based half-open integer interval up to, but not including, 2 is a singleton. (Contributed by Alexander van der Vekens, 31-Jan-2018)

Ref Expression
Assertion fzo12sn
|- ( 1 ..^ 2 ) = { 1 }

Proof

Step Hyp Ref Expression
1 df-2
 |-  2 = ( 1 + 1 )
2 1 oveq2i
 |-  ( 1 ..^ 2 ) = ( 1 ..^ ( 1 + 1 ) )
3 1z
 |-  1 e. ZZ
4 fzosn
 |-  ( 1 e. ZZ -> ( 1 ..^ ( 1 + 1 ) ) = { 1 } )
5 3 4 ax-mp
 |-  ( 1 ..^ ( 1 + 1 ) ) = { 1 }
6 2 5 eqtri
 |-  ( 1 ..^ 2 ) = { 1 }