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

Definition df-djud 6996
 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 6975 in the case of functions). Remark: the restrictions to (resp. ) are not necessary since extra stuff would be thrown away in the post-composition with (resp. ), as in df-case 6977, but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.)
Assertion
Ref Expression
df-djud ⊔d inl inr

Detailed syntax breakdown of Definition df-djud
StepHypRef Expression
1 cR . . 3
2 cS . . 3
31, 2cdjud 6995 . 2 ⊔d
4 cinl 6938 . . . . . 6 inl
51cdm 4547 . . . . . 6
64, 5cres 4549 . . . . 5 inl
76ccnv 4546 . . . 4 inl
81, 7ccom 4551 . . 3 inl
9 cinr 6939 . . . . . 6 inr
102cdm 4547 . . . . . 6
119, 10cres 4549 . . . . 5 inr
1211ccnv 4546 . . . 4 inr
132, 12ccom 4551 . . 3 inr
148, 13cun 3074 . 2 inl inr
153, 14wceq 1332 1 ⊔d inl inr
 Colors of variables: wff set class This definition is referenced by:  djufun  6997  djudm  6998  djuinj  6999
 Copyright terms: Public domain W3C validator