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

Definition df-case 7096
Description: The "case" construction: if  F : A --> X and  G : B --> X are functions, then case ( F ,  G
) : ( A B ) --> X is the natural function obtained by a definition by cases, hence the name. It is the unique function whose existence is asserted by the universal property of disjoint unions updjud 7094. The definition is adapted to make sense also for binary relations (where the universal property also holds). (Contributed by MC and BJ, 10-Jul-2022.)
Assertion
Ref Expression
df-case  |- case ( R ,  S )  =  ( ( R  o.  `'inl )  u.  ( S  o.  `'inr )
)

Detailed syntax breakdown of Definition df-case
StepHypRef Expression
1 cR . . 3  class  R
2 cS . . 3  class  S
31, 2cdjucase 7095 . 2  class case ( R ,  S )
4 cinl 7057 . . . . 5  class inl
54ccnv 4637 . . . 4  class  `'inl
61, 5ccom 4642 . . 3  class  ( R  o.  `'inl )
7 cinr 7058 . . . . 5  class inr
87ccnv 4637 . . . 4  class  `'inr
92, 8ccom 4642 . . 3  class  ( S  o.  `'inr )
106, 9cun 3139 . 2  class  ( ( R  o.  `'inl )  u.  ( S  o.  `'inr ) )
113, 10wceq 1363 1  wff case ( R ,  S )  =  ( ( R  o.  `'inl )  u.  ( S  o.  `'inr )
)
Colors of variables: wff set class
This definition is referenced by:  casefun  7097  casedm  7098  caserel  7099  caseinj  7101  caseinl  7103  caseinr  7104
  Copyright terms: Public domain W3C validator