ILE Home 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  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 6975 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 6977, 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
StepHypRef Expression
1 cR . . 3  class  R
2 cS . . 3  class  S
31, 2cdjud 6995 . 2  class  ( R ⊔d  S )
4 cinl 6938 . . . . . 6  class inl
51cdm 4547 . . . . . 6  class  dom  R
64, 5cres 4549 . . . . 5  class  (inl  |`  dom  R
)
76ccnv 4546 . . . 4  class  `' (inl  |`  dom  R )
81, 7ccom 4551 . . 3  class  ( R  o.  `' (inl  |`  dom  R
) )
9 cinr 6939 . . . . . 6  class inr
102cdm 4547 . . . . . 6  class  dom  S
119, 10cres 4549 . . . . 5  class  (inr  |`  dom  S
)
1211ccnv 4546 . . . 4  class  `' (inr  |`  dom  S )
132, 12ccom 4551 . . 3  class  ( S  o.  `' (inr  |`  dom  S
) )
148, 13cun 3074 . 2  class  ( ( R  o.  `' (inl  |`  dom  R ) )  u.  ( S  o.  `' (inr  |`  dom  S
) ) )
153, 14wceq 1332 1  wff  ( R ⊔d  S )  =  ( ( R  o.  `' (inl  |`  dom  R ) )  u.  ( S  o.  `' (inr  |`  dom  S
) ) )
Colors of variables: wff set class
This definition is referenced by:  djufun  6997  djudm  6998  djuinj  6999
  Copyright terms: Public domain W3C validator