Definition df-case 7049

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 7047. 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 7048	. 2 class case(𝑅, 𝑆)
4		cinl 7010	. . . . 5 class inl
5	4	ccnv 4603	. . . 4 class ◡inl
6	1, 5	ccom 4608	. . 3 class (𝑅 ∘ ◡inl)
7		cinr 7011	. . . . 5 class inr
8	7	ccnv 4603	. . . 4 class ◡inr
9	2, 8	ccom 4608	. . 3 class (𝑆 ∘ ◡inr)
10	6, 9	cun 3114	. 2 class ((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr))
11	3, 10	wceq 1343	1 wff case(𝑅, 𝑆) = ((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr))

This definition is referenced by:  casefun  7050  casedm  7051  caserel  7052  caseinj  7054  caseinl  7056  caseinr  7057