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	$$⊢{\times }_t=\left(r\in \mathrm{V},s\in \mathrm{V}⟼\mathrm{topGen}\left(\mathrm{ran}\left(x\in r,y\in s⟼x\times y\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctx	$$class{\times }_t$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		ctg	$$class\mathrm{topGen}$$
5		vx	$$setvarx$$
6	1	cv	$$setvarr$$
7		vy	$$setvary$$
8	3	cv	$$setvars$$
9	5	cv	$$setvarx$$
10	7	cv	$$setvary$$
11	9 10	cxp	$$class\left(x\times y\right)$$
12	5 7 6 8 11	cmpo	$$class\left(x\in r,y\in s⟼x\times y\right)$$
13	12	crn	$$class\mathrm{ran}\left(x\in r,y\in s⟼x\times y\right)$$
14	13 4	cfv	$$class\mathrm{topGen}\left(\mathrm{ran}\left(x\in r,y\in s⟼x\times y\right)\right)$$
15	1 3 2 2 14	cmpo	$$class\left(r\in \mathrm{V},s\in \mathrm{V}⟼\mathrm{topGen}\left(\mathrm{ran}\left(x\in r,y\in s⟼x\times y\right)\right)\right)$$
16	0 15	wceq	$$wff{\times }_t=\left(r\in \mathrm{V},s\in \mathrm{V}⟼\mathrm{topGen}\left(\mathrm{ran}\left(x\in r,y\in s⟼x\times y\right)\right)\right)$$