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 |) u. ( { 1o } X. tag B ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	bj-c2uple	|- (| A ,, B |)
3	0	bj-c1upl	|- (| A |)
4		c1o	|- 1o
5	4	csn	|- { 1o }
6	1	bj-ctag	|- tag B
7	5 6	cxp	|- ( { 1o } X. tag B )
8	3 7	cun	|- ( (| A |) u. ( { 1o } X. tag B ) )
9	2 8	wceq	|- (| A ,, B |) = ( (| A |) u. ( { 1o } X. tag B ) )