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	⊢ ×t = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( topGen ‘ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctx	⊢ ×t
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		ctg	⊢ topGen
5		vx	⊢ 𝑥
6	1	cv	⊢ 𝑟
7		vy	⊢ 𝑦
8	3	cv	⊢ 𝑠
9	5	cv	⊢ 𝑥
10	7	cv	⊢ 𝑦
11	9 10	cxp	⊢ ( 𝑥 × 𝑦 )
12	5 7 6 8 11	cmpo	⊢ ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) )
13	12	crn	⊢ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) )
14	13 4	cfv	⊢ ( topGen ‘ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) )
15	1 3 2 2 14	cmpo	⊢ ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( topGen ‘ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ) )
16	0 15	wceq	⊢ ×t = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ( topGen ‘ ran ( 𝑥 ∈ 𝑟 , 𝑦 ∈ 𝑠 ↦ ( 𝑥 × 𝑦 ) ) ) )