Metamath Proof Explorer

Theorem dya2iocrfn

Description: The function returning dyadic square covering for a given size has domain ( ran I X. ran I ) . (Contributed by Thierry Arnoux, 19-Sep-2017)

		Ref	Expression
	Hypotheses	sxbrsiga.0	$⊢ J = topGen (ran (.))$
		dya2ioc.1	$⊢ I = (x \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}))$
		dya2ioc.2	$⊢ R = (u \in ran I, v \in ran I ⟼ u \times v)$
	Assertion	dya2iocrfn	$⊢ R Fn (ran I \times ran I)$

Proof

Step	Hyp	Ref	Expression
1		sxbrsiga.0	$⊢ J = topGen (ran (.))$
2		dya2ioc.1	$⊢ I = (x \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}))$
3		dya2ioc.2	$⊢ R = (u \in ran I, v \in ran I ⟼ u \times v)$
4		vex	$⊢ u \in V$
5		vex	$⊢ v \in V$
6	4 5	xpex	$⊢ u \times v \in V$
7	3 6	fnmpoi	$⊢ R Fn (ran I \times ran I)$