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

Definition df-cld 20580
Description: Define a function on topologies whose value is the set of closed sets of the topology. (Contributed by NM, 2-Oct-2006.)
Assertion
Ref Expression
df-cld Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗})
Distinct variable group:   𝑥,𝑗

Detailed syntax breakdown of Definition df-cld
StepHypRef Expression
1 ccld 20577 . 2 class Clsd
2 vj . . 3 setvar 𝑗
3 ctop 20464 . . 3 class Top
42cv 1473 . . . . . . 7 class 𝑗
54cuni 4366 . . . . . 6 class 𝑗
6 vx . . . . . . 7 setvar 𝑥
76cv 1473 . . . . . 6 class 𝑥
85, 7cdif 3536 . . . . 5 class ( 𝑗𝑥)
98, 4wcel 1976 . . . 4 wff ( 𝑗𝑥) ∈ 𝑗
105cpw 4107 . . . 4 class 𝒫 𝑗
119, 6, 10crab 2899 . . 3 class {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗}
122, 3, 11cmpt 4637 . 2 class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗})
131, 12wceq 1474 1 wff Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗})
Colors of variables: wff setvar class
This definition is referenced by:  fncld  20583  cldval  20584
  Copyright terms: Public domain W3C validator