Description: Define the disjoint relation predicate, i.e., the disjoint predicate. A disjoint relation is a converse function of the relation by dfdisjALTV , see the comment of df-disjs why we need disjoint relations instead of converse functions anyway.
The element of the class of disjoints and the disjoint predicate are the same, that is ( R e. Disjs <-> Disj R ) when R is a set, see eldisjsdisj . Alternate definitions are dfdisjALTV , ... , dfdisjALTV5 . (Contributed by Peter Mazsa, 17-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-disjALTV | ⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡ 𝑅 ∧ Rel 𝑅 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cR | ⊢ 𝑅 | |
| 1 | 0 | wdisjALTV | ⊢ Disj 𝑅 |
| 2 | 0 | ccnv | ⊢ ◡ 𝑅 |
| 3 | 2 | ccoss | ⊢ ≀ ◡ 𝑅 |
| 4 | 3 | wcnvrefrel | ⊢ CnvRefRel ≀ ◡ 𝑅 |
| 5 | 0 | wrel | ⊢ Rel 𝑅 |
| 6 | 4 5 | wa | ⊢ ( CnvRefRel ≀ ◡ 𝑅 ∧ Rel 𝑅 ) |
| 7 | 1 6 | wb | ⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡ 𝑅 ∧ Rel 𝑅 ) ) |