Replace "rn" by "cdm" (1)

[avekens]

Some theorems having "codomain" in the comment, "rn" in the label, but no "ran" in their statement or hypotheses are renamed ("rn" replaced by "cdm" for "codomain"), see issue #4470:

Label changes:

• ~ffvelrnd -> ~ffvelcdmd (used 1113 times)
• ~ffvelrnda -> ~ffvelcdmda (used 1119 times)
• ~ffvelrni -> ~ffvelcdmi (used 229 times)
• ~ffvelrn -> ~ffvelcdm (used 492 times)

"cdm" added to list of abbreviations (in comment for ~conventions-labels)

[sctfn]

You have a 68,000 line diff in set.mm. Could you please investigate why?

[icecream17]

manually looking at the diff it's just that about 2000 theorems are affected and on average the proofs involved are very large, so 68k

here's a screenshot of halfway through:

I only briefly glanced at the first 10k lines and at various parts but it's all proof diffs. And here's the part of conventions-labels:

[avekens]

Thank you, @icecream17 , for working out the differences. Besides the part of the additional abbreviation in the conventions, there are the following 4 label changes of the theorems :

The rest is actually only changes within proofs (and since the labels became 1 character longer, the proofs had to be reformatted - all done automatically by find and replace and save proof * /C/F ).

[jkingdon]

• ffvelcdm $p |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B ) $=

Suggested change

	17-Dec-24 ffelrnd ffelcdmd
	17-Dec-24 ffelrnda ffelcdmda
	17-Dec-24 ffelrni ffelcdmi
	17-Dec-24 ffelrn ffelcdm
	17-Dec-24 ffvelrnd ffvelcdmd
	17-Dec-24 ffvelrnda ffvelcdmda
	17-Dec-24 ffvelrni ffvelcdmi
	17-Dec-24 ffvelrn ffvelcdm

[jkingdon]

Although I suggested a different naming convention at #4466 (comment) I don't really object to cdm either.

My main comment is that neither the commit message nor the change to changes-set.txt has the correct names (in the sense of the names used in the old and new versions of set.mm).

[avekens]

Although I suggested a different naming convention at #4466 (comment) I don't really object to cdm either.

I think ffvel is not informative enough (element of what?), so I prefer the currently used labels

My main comment is that neither the commit message nor the change to changes-set.txt has the correct names (in the sense of the names used in the old and new versions of set.mm).

You are absolutely right: one typo, and then many times copy&paste .., I'll correct that.