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

Definition df-tx 21175
 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 21173 . 2 class ×t
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 cvv 3173 . . 3 class V
5 vx . . . . . 6 setvar 𝑥
6 vy . . . . . 6 setvar 𝑦
72cv 1474 . . . . . 6 class 𝑟
83cv 1474 . . . . . 6 class 𝑠
95cv 1474 . . . . . . 7 class 𝑥
106cv 1474 . . . . . . 7 class 𝑦
119, 10cxp 5036 . . . . . 6 class (𝑥 × 𝑦)
125, 6, 7, 8, 11cmpt2 6551 . . . . 5 class (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))
1312crn 5039 . . . 4 class ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))
14 ctg 15921 . . . 4 class topGen
1513, 14cfv 5804 . . 3 class (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦)))
162, 3, 4, 4, 15cmpt2 6551 . 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))))
171, 16wceq 1475 1 wff ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))))
 Colors of variables: wff setvar class This definition is referenced by:  txval  21177
 Copyright terms: Public domain W3C validator