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

Step	Hyp	Ref	Expression
1		cR	. . 3 class R
2		cS	. . 3 class S
3	1, 2	cdjucase 7095	. 2 class case ( R , S )
4		cinl 7057	. . . . 5 class inl
5	4	ccnv 4637	. . . 4 class `'inl
6	1, 5	ccom 4642	. . 3 class ( R o. `'inl )
7		cinr 7058	. . . . 5 class inr
8	7	ccnv 4637	. . . 4 class `'inr
9	2, 8	ccom 4642	. . 3 class ( S o. `'inr )
10	6, 9	cun 3139	. 2 class ( ( R o. `'inl ) u. ( S o. `'inr ) )
11	3, 10	wceq 1363	1 wff case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )

This definition is referenced by:  casefun  7097  casedm  7098  caserel  7099  caseinj  7101  caseinl  7103  caseinr  7104