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

Definition df-tx 22105
 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 22103 . 2 class ×t
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 cvv 3500 . . 3 class V
5 vx . . . . . 6 setvar 𝑥
6 vy . . . . . 6 setvar 𝑦
72cv 1529 . . . . . 6 class 𝑟
83cv 1529 . . . . . 6 class 𝑠
95cv 1529 . . . . . . 7 class 𝑥
106cv 1529 . . . . . . 7 class 𝑦
119, 10cxp 5552 . . . . . 6 class (𝑥 × 𝑦)
125, 6, 7, 8, 11cmpo 7152 . . . . 5 class (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))
1312crn 5555 . . . 4 class ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))
14 ctg 16706 . . . 4 class topGen
1513, 14cfv 6354 . . 3 class (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦)))
162, 3, 4, 4, 15cmpo 7152 . 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))))
171, 16wceq 1530 1 wff ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))))
 Colors of variables: wff setvar class This definition is referenced by:  txval  22107
 Copyright terms: Public domain W3C validator