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

Distinct variable group:   𝑠,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-tx

Step	Hyp	Ref	Expression
1		ctx 14488	. 2 class ×t
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 2763	. . 3 class V
5		vx	. . . . . 6 setvar 𝑥
6		vy	. . . . . 6 setvar 𝑦
7	2	cv 1363	. . . . . 6 class 𝑟
8	3	cv 1363	. . . . . 6 class 𝑠
9	5	cv 1363	. . . . . . 7 class 𝑥
10	6	cv 1363	. . . . . . 7 class 𝑦
11	9, 10	cxp 4661	. . . . . 6 class (𝑥 × 𝑦)
12	5, 6, 7, 8, 11	cmpo 5924	. . . . 5 class (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))
13	12	crn 4664	. . . 4 class ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))
14		ctg 12925	. . . 4 class topGen
15	13, 14	cfv 5258	. . 3 class (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))
16	2, 3, 4, 4, 15	cmpo 5924	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))))
17	1, 16	wceq 1364	1 wff ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))))

This definition is referenced by:  txvalex  14490  txval  14491