There are several possibilities for defining out-of-domain behavior of function values. We chose the empty set in large part because it is very convenient to have function values exist unconditionally (fvex and consequently ovex). Another possibility is to define out-of-domain function value to be the universe _V, which has the advantage of providing us with a simple test (sethood) to determine whether we are using the function outside of its domain. Alexander van der Vekens studied an alternate function value definition with this property; see df-afv and associated theorems in his mathbox.
There is a certain philosophical elegance to the df-afv approach that I can appreciate, but from a practical point of view the drawback is that proofs that a function value exists would be significantly longer. The long proof of cnfex (whose author had presumably overlooked ovex) actually illustrates this point nicely - this is the kind of thing we would have to do frequently if we used a function value definition whose out-of-domain behavior evaluated to _V. The unconditional fvex and ovex are used 2783 and 1913 times respectively in set.mm. With df-afv, the size of set.mm would grow considerably and would make function value existence a major part of many otherwise short proofs, obscuring the more important parts of the proof. There was a discussion of df-afv in this thread: https://groups.google.com/g/metamath/c/cteNUppB6A4/m/1qv4j6wyAgAJ Norm On Wednesday, April 21, 2021 at 10:15:04 PM UTC-4 [email protected] wrote: > It is a bit of a strange theorem. I see that it is in Glauco's mathbox > (and referenced a few times), and both the proof and the uses can be > simplified using ovex, but perhaps there is something that they were trying > to avoid (not axioms, the axiom list is a strict subset with the new > proof). Perhaps they can chime in here. > > On Wed, Apr 21, 2021 at 9:48 PM Jim Kingdon <[email protected]> wrote: > >> On 4/21/21 5:37 PM, Kyle Wyonch wrote: >> >> > I was wondering if this shortening [of cnfex] was valid >> >> Short answer is, yes it is valid. >> >> The longer answer is that set.mm defines a function evaluated outside >> its domain to be the empty set which is why >> http://us.metamath.org/mpeuni/fvex.html does not have any conditions. >> >> By contrast, iset.mm does not have the ability to do quite this, so >> instead cnfex would need to use >> http://us.metamath.org/ileuni/funfvex.html or one of the other >> alternatives under fvex at http://us.metamath.org/ileuni/mmil.html#setmm >> >> There is some discussion of this in the "undefined results" section of >> http://us.metamath.org/mpeuni/conventions.html and >> http://us.metamath.org/ileuni/conventions.html >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> > To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/c36661f8-ac06-7264-2dd8-d95a1cb1b41f%40panix.com >> . >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/644950e9-67b9-489b-85f0-532f4cf2a8a6n%40googlegroups.com.
