fzof

Description: Functionality of the half-open integer set function. (Contributed by Stefan O'Rear, 14-Aug-2015)

		Ref	Expression
	Assertion	fzof	$⊢ ..^: ℤ \times ℤ ⟶ 𝒫 ℤ$

Step	Hyp	Ref	Expression
1		fzssz	$⊢ (m \dots n - 1) \subseteq ℤ$
2		ovex	$⊢ (m \dots n - 1) \in V$
3	2	elpw	$⊢ (m \dots n - 1) \in 𝒫 ℤ \leftrightarrow (m \dots n - 1) \subseteq ℤ$
4	1 3	mpbir	$⊢ (m \dots n - 1) \in 𝒫 ℤ$
5	4	rgen2w	$⊢ \forall m \in ℤ \forall n \in ℤ (m \dots n - 1) \in 𝒫 ℤ$
6		df-fzo	$⊢ ..^= (m \in ℤ, n \in ℤ ⟼ (m \dots n - 1))$
7	6	fmpo	$⊢ \forall m \in ℤ \forall n \in ℤ (m \dots n - 1) \in 𝒫 ℤ \leftrightarrow ..^: ℤ \times ℤ ⟶ 𝒫 ℤ$
8	5 7	mpbi	$⊢ ..^: ℤ \times ℤ ⟶ 𝒫 ℤ$

Metamath Proof Explorer