Definition df-case 7424

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 7422. 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

Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2		cS	. . 3 class 𝑆
3	1, 2	cdjucase 7423	. 2 class case(𝑅, 𝑆)
4		cinl 7385	. . . . 5 class inl
5	4	ccnv 4773	. . . 4 class ◡inl
6	1, 5	ccom 4778	. . 3 class (𝑅 ∘ ◡inl)
7		cinr 7386	. . . . 5 class inr
8	7	ccnv 4773	. . . 4 class ◡inr
9	2, 8	ccom 4778	. . 3 class (𝑆 ∘ ◡inr)
10	6, 9	cun 3218	. 2 class ((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr))
11	3, 10	wceq 1402	1 wff case(𝑅, 𝑆) = ((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr))

This definition is used by:  casefun  7425  casedm  7426  caserel  7427  caseinj  7429  caseinl  7431  caseinr  7432