This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (A ⊔︀ B) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cB	$class B$
2	0 1	cdju	$class (A ⊔︀ B)$
3		c0	$class \emptyset$
4	3	csn	$class \{\emptyset\}$
5	4 0	cxp	$class (\{\emptyset\} \times A)$
6		c1o	$class 1_{𝑜}$
7	6	csn	$class \{1_{𝑜}\}$
8	7 1	cxp	$class (\{1_{𝑜}\} \times B)$
9	5 8	cun	$class ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B))$
10	2 9	wceq	$wff (A ⊔︀ B) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)$