Definition df-tx 12422

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 12421	. 2 class ×t
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 2686	. . 3 class V
5		vx	. . . . . 6 setvar 𝑥
6		vy	. . . . . 6 setvar 𝑦
7	2	cv 1330	. . . . . 6 class 𝑟
8	3	cv 1330	. . . . . 6 class 𝑠
9	5	cv 1330	. . . . . . 7 class 𝑥
10	6	cv 1330	. . . . . . 7 class 𝑦
11	9, 10	cxp 4537	. . . . . 6 class (𝑥 × 𝑦)
12	5, 6, 7, 8, 11	cmpo 5776	. . . . 5 class (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))
13	12	crn 4540	. . . 4 class ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))
14		ctg 12135	. . . 4 class topGen
15	13, 14	cfv 5123	. . 3 class (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))
16	2, 3, 4, 4, 15	cmpo 5776	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))))
17	1, 16	wceq 1331	1 wff ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))))

This definition is referenced by:  txvalex  12423  txval  12424