This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℤ$
4		fzosn	$⊢ 1 \in ℤ \to (1 ..^1 + 1) = \{1\}$
5	3 4	ax-mp	$⊢ (1 ..^1 + 1) = \{1\}$
6	2 5	eqtri	$⊢ (1 ..^2) = \{1\}$