Definition df-djud 7444

Description: The "domain-disjoint-union" of two relations: if 𝑅 ⊆ (𝐴 × 𝑋) and 𝑆 ⊆ (𝐵 × 𝑋) are two binary relations, then (𝑅 ⊔_d 𝑆) is the binary relation from (𝐴 ⊔ 𝐵) to 𝑋 having the universal property of disjoint unions (see updjud 7423 in the case of functions).

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

Assertion

Ref	Expression
df-djud	⊢ (𝑅 ⊔d 𝑆) = ((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆)))

Detailed syntax breakdown of Definition df-djud

Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2		cS	. . 3 class 𝑆
3	1, 2	cdjud 7443	. 2 class (𝑅 ⊔d 𝑆)
4		cinl 7386	. . . . . 6 class inl
5	1	cdm 4774	. . . . . 6 class dom 𝑅
6	4, 5	cres 4776	. . . . 5 class (inl ↾ dom 𝑅)
7	6	ccnv 4773	. . . 4 class ◡(inl ↾ dom 𝑅)
8	1, 7	ccom 4778	. . 3 class (𝑅 ∘ ◡(inl ↾ dom 𝑅))
9		cinr 7387	. . . . . 6 class inr
10	2	cdm 4774	. . . . . 6 class dom 𝑆
11	9, 10	cres 4776	. . . . 5 class (inr ↾ dom 𝑆)
12	11	ccnv 4773	. . . 4 class ◡(inr ↾ dom 𝑆)
13	2, 12	ccom 4778	. . 3 class (𝑆 ∘ ◡(inr ↾ dom 𝑆))
14	8, 13	cun 3218	. 2 class ((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆)))
15	3, 14	wceq 1402	1 wff (𝑅 ⊔d 𝑆) = ((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆)))

This definition is used by:  djufun  7445  djudm  7446  djuinj  7447