Definition df-djud 7059

Description: The "domain-disjoint-union" of two relations: if R C_ ( A X. X ) and S C_ ( B X. X ) are two binary relations, then ( R ⊔d S ) is the binary relation from ( A ⊔ B ) to X having the universal property of disjoint unions (see updjud 7038 in the case of functions).

Remark: the restrictions to dom R (resp. dom S) are not necessary since extra stuff would be thrown away in the post-composition with R (resp. S), as in df-case 7040, but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.)

Assertion

Ref	Expression
df-djud	|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )

Detailed syntax breakdown of Definition df-djud

Step	Hyp	Ref	Expression
1		cR	. . 3 class R
2		cS	. . 3 class S
3	1, 2	cdjud 7058	. 2 class ( R ⊔d S )
4		cinl 7001	. . . . . 6 class inl
5	1	cdm 4598	. . . . . 6 class dom R
6	4, 5	cres 4600	. . . . 5 class (inl |` dom R )
7	6	ccnv 4597	. . . 4 class `' (inl |` dom R )
8	1, 7	ccom 4602	. . 3 class ( R o. `' (inl |` dom R ) )
9		cinr 7002	. . . . . 6 class inr
10	2	cdm 4598	. . . . . 6 class dom S
11	9, 10	cres 4600	. . . . 5 class (inr |` dom S )
12	11	ccnv 4597	. . . 4 class `' (inr |` dom S )
13	2, 12	ccom 4602	. . 3 class ( S o. `' (inr |` dom S ) )
14	8, 13	cun 3109	. 2 class ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
15	3, 14	wceq 1342	1 wff ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )

This definition is referenced by:  djufun  7060  djudm  7061  djuinj  7062