Replace "rn" by "cdm" in labels for theorems about codomains

[avekens]

There are some theorems about codomains (and not ranges) of functions which have an "rn" (for "range") in its labels. These fragments should be replaced by "cdm" (for "codomain"), and "cdm" should be added to the list of abbreviations.

Labels which are concerned (having "codomain" in the comment, "rn" in the label, but no "ran" in its statement or hypotheses):

• ~foelrni
• ~ffvelrn
• ~ffvelrni
• ~ffvelrnda
• ~ffvelrnd
• ~fvmptelrn
• ~frnssb
• ~fovrn
• ~fovrnda
• ~fovrnd
• ~fornex
• ~frnsuppeq
• ~frnsuppeqg
• ~frnfsuppbi
• ~cncffvrn
• ~fafvelrn
• ~fafv2elrn
• ~frnvafv2v

[avekens]

See discussion in PR #4466:

@icecream17 :

Incidentally, metamath seems to use range more often than codomain. I only just seen that there was a difference:

Codomain: The set of all possible output values that a function could produce
Range: The subset of those values that the function actually does produce
https://math.stackexchange.com/questions/3317941/what-is-the-difference-between-codomain-and-range

This means ~ frn and such is somewhat of a misnomer?

@BTernaryTau

frn is fine since it explicitly deals with the function's range. foelrni is a better example since the statement doesn't reference the function's range and its description refers to the codomain. However, since it's about onto functions, the range and codomain are equal, so I don't think this is a big deal. The problem case (in my opinion) is theorems like ffvelrn and frnssb that don't deal with the range, only the codomain.

@jkingdon :

The good news is that the comments correctly refer to the codomain and don't contain the word "range", which doesn't apply here.

Whether we want to rename them to something not containing rn I guess I don't have a strong opinion about. Maybe they could just be called ffvel and ssf (or something else with an f in it). The name fragment f refers to F : X --> Y notation and thus means that the theorem will be specifying a codomain (in this example Y).

@avekens :

Maybe we should replace "rn" by "cdm" in the label in such cases, like here done with ~f1cdmsn, or also other theorems in set.mm (e.g., ~focdmex).

[jkingdon]

If the function is onto, codomain and range are identical and I'd probably rather tend towards the range terminology.