Definition df-dju

Description: Disjoint union of two classes. This is a way of creating a set which contains elements corresponding to each element of A or B , tagging each one with whether it came from A or B . (Contributed by Jim Kingdon, 20-Jun-2022)

	Ref	Expression
Assertion	df-dju	⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	cdju	⊢ ( 𝐴 ⊔ 𝐵 )
3		c0	⊢ ∅
4	3	csn	⊢ { ∅ }
5	4 0	cxp	⊢ ( { ∅ } × 𝐴 )
6		c1o	⊢ 1o
7	6	csn	⊢ { 1o }
8	7 1	cxp	⊢ ( { 1o } × 𝐵 )
9	5 8	cun	⊢ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
10	2 9	wceq	⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )