Definition df-tx

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctx	|- tX
1		vr	|- r
2		cvv	|- _V
3		vs	|- s
4		ctg	|- topGen
5		vx	|- x
6	1	cv	|- r
7		vy	|- y
8	3	cv	|- s
9	5	cv	|- x
10	7	cv	|- y
11	9 10	cxp	|- ( x X. y )
12	5 7 6 8 11	cmpo	|- ( x e. r , y e. s |-> ( x X. y ) )
13	12	crn	|- ran ( x e. r , y e. s |-> ( x X. y ) )
14	13 4	cfv	|- ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) )
15	1 3 2 2 14	cmpo	|- ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
16	0 15	wceq	|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )