MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tx Structured version   Visualization version   GIF version

Definition df-tx 22100
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
StepHypRef Expression
1 ctx 22098 . 2 class ×t
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 cvv 3495 . . 3 class V
5 vx . . . . . 6 setvar 𝑥
6 vy . . . . . 6 setvar 𝑦
72cv 1527 . . . . . 6 class 𝑟
83cv 1527 . . . . . 6 class 𝑠
95cv 1527 . . . . . . 7 class 𝑥
106cv 1527 . . . . . . 7 class 𝑦
119, 10cxp 5547 . . . . . 6 class (𝑥 × 𝑦)
125, 6, 7, 8, 11cmpo 7147 . . . . 5 class (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))
1312crn 5550 . . . 4 class ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))
14 ctg 16701 . . . 4 class topGen
1513, 14cfv 6349 . . 3 class (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦)))
162, 3, 4, 4, 15cmpo 7147 . 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))))
171, 16wceq 1528 1 wff ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  txval  22102
  Copyright terms: Public domain W3C validator