Definition df-tx 17547

Description: Define the binary topological product, which is homeomorphic to the general topological product over a two element set, but is more convenient to use. (Contributed by Jeff Madsen, 2-Sep-2009.)

Assertion

Ref	Expression
df-tx	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )

Distinct variable group:   s, r, x, y

Detailed syntax breakdown of Definition df-tx

Step	Hyp	Ref	Expression
1		ctx 17545	. 2 class tX
2		vr	. . 3 set r
3		vs	. . 3 set s
4		cvv 2916	. . 3 class _V
5		vx	. . . . . 6 set x
6		vy	. . . . . 6 set y
7	2	cv 1648	. . . . . 6 class r
8	3	cv 1648	. . . . . 6 class s
9	5	cv 1648	. . . . . . 7 class x
10	6	cv 1648	. . . . . . 7 class y
11	9, 10	cxp 4835	. . . . . 6 class ( x X. y )
12	5, 6, 7, 8, 11	cmpt2 6042	. . . . 5 class ( x e. r , y e. s |-> ( x X. y ) )
13	12	crn 4838	. . . 4 class ran ( x e. r , y e. s |-> ( x X. y ) )
14		ctg 13620	. . . 4 class topGen
15	13, 14	cfv 5413	. . 3 class ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) )
16	2, 3, 4, 4, 15	cmpt2 6042	. 2 class ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
17	1, 16	wceq 1649	1 wff tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )

This definition is referenced by:  txval  17549