Definition df-tx 23066

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 23064	. 2 class ×t
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3475	. . 3 class V
5		vx	. . . . . 6 setvar 𝑥
6		vy	. . . . . 6 setvar 𝑦
7	2	cv 1541	. . . . . 6 class 𝑟
8	3	cv 1541	. . . . . 6 class 𝑠
9	5	cv 1541	. . . . . . 7 class 𝑥
10	6	cv 1541	. . . . . . 7 class 𝑦
11	9, 10	cxp 5675	. . . . . 6 class (𝑥 × 𝑦)
12	5, 6, 7, 8, 11	cmpo 7411	. . . . 5 class (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))
13	12	crn 5678	. . . 4 class ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))
14		ctg 17383	. . . 4 class topGen
15	13, 14	cfv 6544	. . 3 class (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))
16	2, 3, 4, 4, 15	cmpo 7411	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))))
17	1, 16	wceq 1542	1 wff ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦))))

This definition is referenced by:  txval  23068