Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-disjALTV | Structured version Visualization version GIF version |
Description: Define the disjoint
relation predicate, i.e., the disjoint predicate. A
disjoint relation is a converse function of the relation by dfdisjALTV 36561,
see the comment of df-disjs 36552 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 (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 36575. Alternate definitions are dfdisjALTV 36561, ... , dfdisjALTV5 36565. (Contributed by Peter Mazsa, 17-Jul-2021.) |
Ref | Expression |
---|---|
df-disjALTV | ⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cR | . . 3 class 𝑅 | |
2 | 1 | wdisjALTV 36104 | . 2 wff Disj 𝑅 |
3 | 1 | ccnv 5550 | . . . . 5 class ◡𝑅 |
4 | 3 | ccoss 36070 | . . . 4 class ≀ ◡𝑅 |
5 | 4 | wcnvrefrel 36079 | . . 3 wff CnvRefRel ≀ ◡𝑅 |
6 | 1 | wrel 5556 | . . 3 wff Rel 𝑅 |
7 | 5, 6 | wa 399 | . 2 wff ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅) |
8 | 2, 7 | wb 209 | 1 wff ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅)) |
Colors of variables: wff setvar class |
This definition is referenced by: dfdisjALTV 36561 dfdisjALTV2 36562 eldisjsdisj 36575 disjrel 36578 |
Copyright terms: Public domain | W3C validator |