Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-tx GIF version

Definition df-tx 12484
 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 12483 . 2 class ×t
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 cvv 2690 . . 3 class V
5 vx . . . . . 6 setvar 𝑥
6 vy . . . . . 6 setvar 𝑦
72cv 1331 . . . . . 6 class 𝑟
83cv 1331 . . . . . 6 class 𝑠
95cv 1331 . . . . . . 7 class 𝑥
106cv 1331 . . . . . . 7 class 𝑦
119, 10cxp 4547 . . . . . 6 class (𝑥 × 𝑦)
125, 6, 7, 8, 11cmpo 5786 . . . . 5 class (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))
1312crn 4550 . . . 4 class ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))
14 ctg 12197 . . . 4 class topGen
1513, 14cfv 5133 . . 3 class (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦)))
162, 3, 4, 4, 15cmpo 5786 . 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))))
171, 16wceq 1332 1 wff ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥𝑟, 𝑦𝑠 ↦ (𝑥 × 𝑦))))
 Colors of variables: wff set class This definition is referenced by:  txvalex  12485  txval  12486
 Copyright terms: Public domain W3C validator