Definition df-djud 7101

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 7080 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 7082, 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 7100	. 2 class ( R ⊔d S )
4		cinl 7043	. . . . . 6 class inl
5	1	cdm 4626	. . . . . 6 class dom R
6	4, 5	cres 4628	. . . . 5 class (inl |` dom R )
7	6	ccnv 4625	. . . 4 class `' (inl |` dom R )
8	1, 7	ccom 4630	. . 3 class ( R o. `' (inl |` dom R ) )
9		cinr 7044	. . . . . 6 class inr
10	2	cdm 4626	. . . . . 6 class dom S
11	9, 10	cres 4628	. . . . 5 class (inr |` dom S )
12	11	ccnv 4625	. . . 4 class `' (inr |` dom S )
13	2, 12	ccom 4630	. . 3 class ( S o. `' (inr |` dom S ) )
14	8, 13	cun 3127	. 2 class ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
15	3, 14	wceq 1353	1 wff ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )

This definition is referenced by:  djufun  7102  djudm  7103  djuinj  7104