Add imadomnum, and drop the ax-ac dependency from fimact

[vince-gonzalez]

This frees nothing on its own, and with fimactOLD kept it does not move the
count at all: 473 statements reach ax-ac/ax-ac2 before and after, because
the old proof retained under fimactOLD still goes through imadomg. Same
arithmetic as #5458, where keeping the two OLD copies took 55 down to 53.

It is worth having for the lemma.

imadomnum

set.mm states dominance of an image by its index set three times and gives the
well-orderable-domain version of only two:

general, uses choice	well-orderable domain
fodomg	fodomnum
fnrndomg	fnrndomnum (#5443)
imadomg	missing

imadomnum is the missing one, stated in exactly imadomg's shape with
A e. B weakened to A e. dom card, the same way fnrndomnum relates to
fnrndomg.

Two things about it are deliberate.

It goes through fodomnum, not fnrndomnum. fnrndomnum is at line
118104 of develop and fimact at 118098, six lines above it, so an
imadomnum proved from fnrndomnum could not be placed anywhere fimact
could cite it and one of the two would have to move. fodomnum is at 109793,
before both. Since fnrndomnum is itself only dffn4 then fodomnum, going
straight to fodomnum costs nothing and moves no statement.

It is curried rather than conjoined. Its two siblings in the main part are
curried, and the conjoined precedent, imadomfi, is in a mathbox and so cannot
be named from here.

The route never needs a surjection of its own. Restricting F to A gives a
function on ( A i^i dom F ); that set is a subset of a well-orderable set
and so well-orderable by ssnum; dffn4 turns the Fn into an onto and
fodomnum bounds the range. Rewriting ran ( F | A ) as ( F " A ) and composing with ( A i^i dom F ) ~<_ A ` finishes it.

fimact

The first caller. A ~<_ _om is a hypothesis, so omelon and ondomen give
A e. dom card and imadomnum applies where imadomg was used. 71 steps to
108.

fimactOLD keeps the previous proof, following fnctOLD and dmctOLD from
#5458. discouraged regenerated: two lines added, none removed.

Why it is worth landing anyway

fimact is one of four remaining callers of these three lemmas that hold a
hypothesis making their own domain well-orderable. Measured together the four
free 134 statements; measured one at a time they free 60, 49, 1 and 1. Where
several of them feed one subtree, each reads near zero alone and the subtree
only leaves the cone when the last one goes. fimact is one of the ones that
reads as 1.

imadomnum is also the lemma the other three need in order to be stated
without choice, in the same way #5443 froze nothing by itself.

Checks run

• verify proof * on the whole database, no errors
• verify markup *, no errors
• scripts/rewrap applied, so the file is in canonical form
• scripts/regen-discouraged, two lines added for fimactOLD
• the diff touches one new statement, one reproved statement, and its OLD copy