Many theorems in set.mm are characterizations of elements of a defined
class. For instance: ~isgrp , ~ istopg . More precisely, if we have a
definition
df-xxx $a |- Class = { x | Phi } $.
Then there is typically in set.mm a theorem isxxx. If Phi(A) does not
imply that A is a set, then there are two possible forms:
isxxx1 $p |- ( A e. Class <-> ( A e. _V /\ Phi(A) ) )
isxxx2 $p |- ( A e. V -> ( A e. Class <-> Phi(A) ) )
It is easy to go back and forth (using biadan2 and baib).
Is there a preferred form ? Is it ok to have both in set.mm ? It seems to
me that isxxx1 is closer to a real characterization (while isxxx2 is a
characterization among sets), but after a quick look, it seems that isxxx2
is often (majoritarily?) used in set.mm, for instance by looking at the
number of usages of elab2g versus elab4g.
Benoît
--
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/f8248f4c-ea12-4b44-b6e7-dee1e5db3feen%40googlegroups.com.
