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

Definition df-cld 12323
 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 12320 . 2 class Clsd
2 vj . . 3 setvar 𝑗
3 ctop 12223 . . 3 class Top
42cv 1331 . . . . . . 7 class 𝑗
54cuni 3745 . . . . . 6 class 𝑗
6 vx . . . . . . 7 setvar 𝑥
76cv 1331 . . . . . 6 class 𝑥
85, 7cdif 3074 . . . . 5 class ( 𝑗𝑥)
98, 4wcel 1481 . . . 4 wff ( 𝑗𝑥) ∈ 𝑗
105cpw 3516 . . . 4 class 𝒫 𝑗
119, 6, 10crab 2421 . . 3 class {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗}
122, 3, 11cmpt 3998 . 2 class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗})
131, 12wceq 1332 1 wff Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 𝑗 ∣ ( 𝑗𝑥) ∈ 𝑗})
 Colors of variables: wff set class This definition is referenced by:  fncld  12326  cldval  12327
 Copyright terms: Public domain W3C validator