Definition df-bj-2upl

Description: Definition of the Morse couple. See df-bj-1upl . New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq , bj-2uplth , bj-2uplex , and the properties of the projections (see df-bj-pr1 and df-bj-pr2 ). (Contributed by BJ, 6-Oct-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	df-bj-2upl	$$⊢⦅A,B⦆=⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	bj-c2uple	$$class⦅A,B⦆$$
3	0	bj-c1upl	$$class⦅A⦆$$
4		c1o	$$class{1}_{𝑜}$$
5	4	csn	$$class\left\{1_{𝑜}\right\}$$
6	1	bj-ctag	$$classtagB$$
7	5 6	cxp	$$class\left(\left\{1_{𝑜}\right\}\times tagB\right)$$
8	3 7	cun	$$class\left(⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)\right)$$
9	2 8	wceq	$$wff⦅A,B⦆=⦅A⦆\cup \left(\left\{1_{𝑜}\right\}\times tagB\right)$$