Okay, thank you, I see the difference. Am 14.12.2024 um 21:04 schrieb Mario Carneiro:
`Disj_ x e. A B` is about disjointness of an *indexed family* of sets B(x), where x ranges over the index set A. It says that if B(x) and B(y) share a common element, then x = y. This is a stronger notion than disjointness of a set of sets, which is what your _disj_ does, since here you can conclude only that if B(x) and B(y) share a common element then B(x) = B(y). For example, a family of empty sets of any cardinality is a disjoint family, and a family of sets x e. A |-> { 0 } is disjoint if and only if A has at most one element. You cannot express the latter theorem using _disj_, because if you try to convert the indexed family into a set of sets you just get { { 0 } } (or (/) if A is empty) which is a disjoint family of sets.Conversely, you can define _disj_ in terms of Disj_ though: _disj_ A <-> Disj x e. A x . On Sat, Dec 14, 2024 at 8:57 PM 'Peter Dolland' via Metamath <[email protected]> wrote: Can anybody help me to understand the definition of Disjointness: df-disj $a |- ( Disj_ x e. A B <-> A. y E* x e. A y e. B ) $. ? What means x, A, and B here? What about my alternative definition as 1-ary predicate: _disj_ A <-> A. B e. A A. C e. A ( B = C \/ B i^i C = (/) ) ? Would it be provable: $p _disj_ A <-> Disj_ x e. A B $= ? $. ? Thank you for your help! -- 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] <mailto:metamath%[email protected]>. To view this discussion visit https://groups.google.com/d/msgid/metamath/63763d29-b77a-4586-8664-74882baeaca6%40gmx.de. -- 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 visit https://groups.google.com/d/msgid/metamath/CAFXXJStPS%3D0DJ4vh7LfkhzD1V4NSUG3W8%3DXJe6q8Osdmc2_6WQ%40mail.gmail.com <https://groups.google.com/d/msgid/metamath/CAFXXJStPS%3D0DJ4vh7LfkhzD1V4NSUG3W8%3DXJe6q8Osdmc2_6WQ%40mail.gmail.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 visit https://groups.google.com/d/msgid/metamath/abb14785-ebff-4e17-968d-66b83c19ce6e%40gmx.de.
