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 20871
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 20868 . 2 class Clsd
2 vj . . 3 setvar 𝑗
3 ctop 20746 . . 3 class Top
42cv 1522 . . . . . . 7 class 𝑗
54cuni 4468 . . . . . 6 class 𝑗
6 vx . . . . . . 7 setvar 𝑥
76cv 1522 . . . . . 6 class 𝑥
85, 7cdif 3604 . . . . 5 class ( 𝑗𝑥)
98, 4wcel 2030 . . . 4 wff ( 𝑗𝑥) ∈ 𝑗
105cpw 4191 . . . 4 class 𝒫 𝑗
119, 6, 10crab 2945 . . 3 class {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗}
122, 3, 11cmpt 4762 . 2 class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗})
131, 12wceq 1523 1 wff Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗})
Colors of variables: wff setvar class
This definition is referenced by:  fncld  20874  cldval  20875
  Copyright terms: Public domain W3C validator