Disjointness in set.mm

[Peter Dolland]

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!

[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 .

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/63763d29-b77a-4586-8664-74882baeaca6%40gmx.de.

[Peter Dolland]

Okay, thank you, I see the difference.

To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJStPS%3D0DJ4vh7LfkhzD1V4NSUG3W8%3DXJe6q8Osdmc2_6WQ%40mail.gmail.com.

[Peter Dolland]

However, I would prefer to define the disjointness of an *indexed family* by ensuring the injectivness of the index map:

_iDisj_ iMap <-> ( Fun `' iMap /\  _disj_ ran iMap )

What do you think about?

[Mario Carneiro]

That doesn't match the other of the two examples I gave: the family x e. A |-> (/) is always a disjoint family. This is not injective as a function because (/) is returned many times.

[Peter Dolland]

Okay, thank you for the hint! I think, I want to exclude empty sets in the family with my definition of _iDisj_ . So we would have an equivalence only for this case.

$p ( ( -. (/) e. ran B ) -> ( _iDisj_ B <-> Disj_ x e. A B ) ) $= ? $.