fzf

Description: Establish the domain and codomain of the finite integer sequence function. (Contributed by Scott Fenton, 8-Aug-2013) (Revised by Mario Carneiro, 16-Nov-2013)

		Ref	Expression
	Assertion	fzf	$⊢ \dots : ℤ \times ℤ ⟶ 𝒫 ℤ$

Proof

Step	Hyp	Ref	Expression
1		zex	$⊢ ℤ \in V$
2		ssrab2	$⊢ \{k \in ℤ \| (m \leq k \land k \leq n)\} \subseteq ℤ$
3	1 2	elpwi2	$⊢ \{k \in ℤ \| (m \leq k \land k \leq n)\} \in 𝒫 ℤ$
4	3	rgen2w	$⊢ \forall m \in ℤ \forall n \in ℤ \{k \in ℤ \| (m \leq k \land k \leq n)\} \in 𝒫 ℤ$
5		df-fz	$⊢ \dots = (m \in ℤ, n \in ℤ ⟼ \{k \in ℤ \| (m \leq k \land k \leq n)\})$
6	5	fmpo	$⊢ \forall m \in ℤ \forall n \in ℤ \{k \in ℤ \| (m \leq k \land k \leq n)\} \in 𝒫 ℤ \leftrightarrow \dots : ℤ \times ℤ ⟶ 𝒫 ℤ$
7	4 6	mpbi	$⊢ \dots : ℤ \times ℤ ⟶ 𝒫 ℤ$

Metamath Proof Explorer

Theorem fzf

Proof