`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]. > 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.
