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 ∈ ℤ
4 fzosn ( 1 ∈ ℤ → ( 1 ..^ ( 1 + 1 ) ) = { 1 } )
5 3 4 ax-mp ( 1 ..^ ( 1 + 1 ) ) = { 1 }
6 2 5 eqtri ( 1 ..^ 2 ) = { 1 }