Another thing I find confusing are the braces around ℤ × ℤ. They seem to be unnecessary (it wouldn’t make much sense for ∈ to have higher precedence than ×), and/or would imply a singleton set containing the set ℤ × ℤ as its only element.
Unicode actually has semantic symbols that could be used for a nicer 2D monospaced layout here, such as ⎧ ⎪ ⎨ ⎩ ( (LEFT CURLY BRACKET UPPER HOOK, MIDDLE PIECE, LOWER HOOK, and CURLY BRACKET EXTENSION). With more conditional rows, you could use these. One downside is that you would have to do a 2D parse, since the = wouldn't be on the first line. We've been loath to go there. It also seems painful as a user to have to type all the right bracket symbols in all the right places.
We do support the Unicode ⎡|⎦ symbols for matrices. The grammar is that a matrix starts with either [ or ⎡ and ends with either ] or ⎦. Rows can be optionally surrounded by |. I find this too cumbersome to use myself.
Another thing I find confusing are the braces around ℤ × ℤ. They seem to be unnecessary (it wouldn’t make much sense for ∈ to have higher precedence than ×), and/or would imply a singleton set containing the set ℤ × ℤ as its only element.