Definition df-tx 14489

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 14488	. 2 class tX
2		vr	. . 3 setvar r
3		vs	. . 3 setvar s
4		cvv 2763	. . 3 class _V
5		vx	. . . . . 6 setvar x
6		vy	. . . . . 6 setvar y
7	2	cv 1363	. . . . . 6 class r
8	3	cv 1363	. . . . . 6 class s
9	5	cv 1363	. . . . . . 7 class x
10	6	cv 1363	. . . . . . 7 class y
11	9, 10	cxp 4661	. . . . . 6 class ( x X. y )
12	5, 6, 7, 8, 11	cmpo 5924	. . . . 5 class ( x e. r , y e. s |-> ( x X. y ) )
13	12	crn 4664	. . . 4 class ran ( x e. r , y e. s |-> ( x X. y ) )
14		ctg 12925	. . . 4 class topGen
15	13, 14	cfv 5258	. . 3 class ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) )
16	2, 3, 4, 4, 15	cmpo 5924	. 2 class ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
17	1, 16	wceq 1364	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:  txvalex  14490  txval  14491