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

Definition df-case 6972
 Description: The "case" construction: if 𝐹:𝐴⟶𝑋 and 𝐺:𝐵⟶𝑋 are functions, then case(𝐹, 𝐺):(𝐴 ⊔ 𝐵)⟶𝑋 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 6970. 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(𝑅, 𝑆) = ((𝑅inl) ∪ (𝑆inr))

Detailed syntax breakdown of Definition df-case
StepHypRef Expression
1 cR . . 3 class 𝑅
2 cS . . 3 class 𝑆
31, 2cdjucase 6971 . 2 class case(𝑅, 𝑆)
4 cinl 6933 . . . . 5 class inl
54ccnv 4541 . . . 4 class inl
61, 5ccom 4546 . . 3 class (𝑅inl)
7 cinr 6934 . . . . 5 class inr
87ccnv 4541 . . . 4 class inr
92, 8ccom 4546 . . 3 class (𝑆inr)
106, 9cun 3069 . 2 class ((𝑅inl) ∪ (𝑆inr))
113, 10wceq 1331 1 wff case(𝑅, 𝑆) = ((𝑅inl) ∪ (𝑆inr))
 Colors of variables: wff set class This definition is referenced by:  casefun  6973  casedm  6974  caserel  6975  caseinj  6977  caseinl  6979  caseinr  6980
 Copyright terms: Public domain W3C validator