Definition df-disjALTV 36553

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

Assertion

Ref	Expression
df-disjALTV	⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅))

Detailed syntax breakdown of Definition df-disjALTV

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 𝑅))

This definition is referenced by:  dfdisjALTV  36561  dfdisjALTV2  36562  eldisjsdisj  36575  disjrel  36578