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	⊢ ⦅ 𝐴 , 𝐵 ⦆ = ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	bj-c2uple	⊢ ⦅ 𝐴 , 𝐵 ⦆
3	0	bj-c1upl	⊢ ⦅ 𝐴 ⦆
4		c1o	⊢ 1o
5	4	csn	⊢ { 1o }
6	1	bj-ctag	⊢ tag 𝐵
7	5 6	cxp	⊢ ( { 1o } × tag 𝐵 )
8	3 7	cun	⊢ ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) )
9	2 8	wceq	⊢ ⦅ 𝐴 , 𝐵 ⦆ = ( ⦅ 𝐴 ⦆ ∪ ( { 1o } × tag 𝐵 ) )