Definition df-tx 13047

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 13046	. 2 class ×t
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 2730	. . 3 class V
5		vx	. . . . . 6 setvar 𝑥
6		vy	. . . . . 6 setvar 𝑦
7	2	cv 1347	. . . . . 6 class 𝑟
8	3	cv 1347	. . . . . 6 class 𝑠
9	5	cv 1347	. . . . . . 7 class 𝑥
10	6	cv 1347	. . . . . . 7 class 𝑦
11	9, 10	cxp 4609	. . . . . 6 class (𝑥 × 𝑦)
12	5, 6, 7, 8, 11	cmpo 5855	. . . . 5 class (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))
13	12	crn 4612	. . . 4 class ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))
14		ctg 12594	. . . 4 class topGen
15	13, 14	cfv 5198	. . 3 class (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))
16	2, 3, 4, 4, 15	cmpo 5855	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))))
17	1, 16	wceq 1348	1 wff ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))))

This definition is referenced by:  txvalex  13048  txval  13049