Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-djud GIF version

Definition df-djud 6988
 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 6967 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 6969, 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
StepHypRef Expression
1 cR . . 3 class 𝑅
2 cS . . 3 class 𝑆
31, 2cdjud 6987 . 2 class (𝑅d 𝑆)
4 cinl 6930 . . . . . 6 class inl
51cdm 4539 . . . . . 6 class dom 𝑅
64, 5cres 4541 . . . . 5 class (inl ↾ dom 𝑅)
76ccnv 4538 . . . 4 class (inl ↾ dom 𝑅)
81, 7ccom 4543 . . 3 class (𝑅(inl ↾ dom 𝑅))
9 cinr 6931 . . . . . 6 class inr
102cdm 4539 . . . . . 6 class dom 𝑆
119, 10cres 4541 . . . . 5 class (inr ↾ dom 𝑆)
1211ccnv 4538 . . . 4 class (inr ↾ dom 𝑆)
132, 12ccom 4543 . . 3 class (𝑆(inr ↾ dom 𝑆))
148, 13cun 3069 . 2 class ((𝑅(inl ↾ dom 𝑅)) ∪ (𝑆(inr ↾ dom 𝑆)))
153, 14wceq 1331 1 wff (𝑅d 𝑆) = ((𝑅(inl ↾ dom 𝑅)) ∪ (𝑆(inr ↾ dom 𝑆)))
 Colors of variables: wff set class This definition is referenced by:  djufun  6989  djudm  6990  djuinj  6991
 Copyright terms: Public domain W3C validator