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 e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
dya2ioc.2
|- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )
Assertion dya2iocrfn
|- R Fn ( ran I X. ran I )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0
 |-  J = ( topGen ` ran (,) )
2 dya2ioc.1
 |-  I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
3 dya2ioc.2
 |-  R = ( u e. ran I , v e. ran I |-> ( u X. v ) )
4 vex
 |-  u e. _V
5 vex
 |-  v e. _V
6 4 5 xpex
 |-  ( u X. v ) e. _V
7 3 6 fnmpoi
 |-  R Fn ( ran I X. ran I )