Description: Define the disjoint elementhood relation predicate, i.e., the disjoint elementhood predicate. Read: the elements of A are disjoint. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is ( A e. ElDisjs <-> ElDisj A ) when A is a set, see eleldisjseldisj .
As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt with dfeldisj5 . See also the comments of ~? dfmembpart2 and of ~? df-parts . (Contributed by Peter Mazsa, 17-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-eldisj | |- ( ElDisj A <-> Disj ( `' _E |` A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | |- A |
|
| 1 | 0 | weldisj | |- ElDisj A |
| 2 | cep | |- _E |
|
| 3 | 2 | ccnv | |- `' _E |
| 4 | 3 0 | cres | |- ( `' _E |` A ) |
| 5 | 4 | wdisjALTV | |- Disj ( `' _E |` A ) |
| 6 | 1 5 | wb | |- ( ElDisj A <-> Disj ( `' _E |` A ) ) |