It's not excluding `(/)` from being an extensible structure, it is rather
the opposite: it asserts that f with (/) removed is a function. It is
impossible for any set containing (/) to be a function, because a function
is a set of ordered pairs and (/) is not an ordered pair. So this is being
unusually relaxed and letting structures that contain (/) still be
considered structures even if they are not, strictly speaking, functions.
As for why the unusual allowance, this is a trick used to ensure that
expressions like { <. A, B >. , <. C, D >. } are structures without
asserting or implying that A,B,C,D are sets. This is used critically in
strle1, strle2, strle3, strleun to avoid sethood hypotheses on the
"payload" sets: without this, ipsstr and theorems like it will have many
sethood assumptions, and may not even be usable in the empty context.
Instead, the sethood assumption is deferred until it is actually needed,
e.g. ipsbase, which requires that the base set is a set but not any of the
other components.
On Mon, Nov 15, 2021 at 1:08 AM 'Alexander van der Vekens' via Metamath <
[email protected]> wrote:
> I wonder why (/) is/must be excluded from an extensible structure to be a
> function:
>
> df-struct $a |- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\
> Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) } $.
>
> Why Fun ( f \ { (/) } ) and not simply Fun f ?
>
> I searched for a justification in set.mm and also in the google group,
> but I did not find any hint. Formerly, there wasn't such a restriction, see
> https://groups.google.com/g/metamath/c/BFFSR3b5qEo/m/s6vph-zL_DoJ.
>
> Can anybody explain this restriction? Is there any meaningful structure
> which contains the empty set, e .g. S = { (/) , <. ( Base ` ndx ) , B >. ,
> <. ( E ` ndx ) , .+ >. } (will Fun S not hold in this case?)?
>
>
>
>
> --
> 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/8213c12b-c060-4d15-b1d7-62a58536b724n%40googlegroups.com
> <https://groups.google.com/d/msgid/metamath/8213c12b-c060-4d15-b1d7-62a58536b724n%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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/CAFXXJSv%2BWT_y5wEEPer663F%2Bbvo75Ec4hZCNQ9Fa9hhHbvyRDA%40mail.gmail.com.
