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	⊢ 𝐽 = ( topGen ‘ ran (,) )
	dya2ioc.1	⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
	dya2ioc.2	⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
Assertion	dya2iocrfn	⊢ 𝑅 Fn ( ran 𝐼 × ran 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		sxbrsiga.0	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		dya2ioc.1	⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3		dya2ioc.2	⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
4		vex	⊢ 𝑢 ∈ V
5		vex	⊢ 𝑣 ∈ V
6	4 5	xpex	⊢ ( 𝑢 × 𝑣 ) ∈ V
7	3 6	fnmpoi	⊢ 𝑅 Fn ( ran 𝐼 × ran 𝐼 )