[grandDesigns]

In {f ∈ [1..N ⟶ 1..N] : ∀ y ∈ 1..N : ∃ x ∈ 1..N : f[x]=y}

What does the colon : mean?

It used to be that:

| = given that

, = and

but, I have never seen a : used in math.

[AstralStorm]

It is TLA+, not quite typical math notation. Lambda and list comprehension notations are more common.

[tnecniv]

Same as |. Like many things in math, there's a wildly accepted notations.

[LeanderK]

just syntax. Some leave them out, some choose colons, i've seen dots in formal systems (∀y.∀x.(x=y)) etc.