Thank you, Mario, for your explanation. It sounds reasonable, although it
is more difficult to proof certain theorems for arbitrary extensible
structures: Since we cannot assume Fun S if S struct X (only Fun ( S \ {
(/) } ), see ~ structn0fun, or equivalently Fun `' `' S, see ~
structfung), special versions of theorems with antecedent Fun F are needed
(see, for example, ~fundmge2nop0 vs. ~fundmge2nop).
I plan to add this explanation to the comment within set.mm, so that it is
documented for everybody and for the future.
Alexander
On Monday, November 15, 2021 at 8:38:26 AM UTC+1 [email protected] wrote:
> 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/ad158986-1105-4e5e-a7f4-b35584996694n%40googlegroups.com.
