Definition df-bj-2upl 35892

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

Assertion

Ref	Expression
df-bj-2upl	⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵))

Detailed syntax breakdown of Definition df-bj-2upl

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	bj-c2uple 35891	. 2 class ⦅𝐴, 𝐵⦆
4	1	bj-c1upl 35878	. . 3 class ⦅𝐴⦆
5		c1o 8459	. . . . 5 class 1o
6	5	csn 4629	. . . 4 class {1o}
7	2	bj-ctag 35855	. . . 4 class tag 𝐵
8	6, 7	cxp 5675	. . 3 class ({1o} × tag 𝐵)
9	4, 8	cun 3947	. 2 class (⦅𝐴⦆ ∪ ({1o} × tag 𝐵))
10	3, 9	wceq 1542	1 wff ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵))

This definition is referenced by:  bj-2upleq  35893  bj-pr21val  35894  bj-pr22val  35900  bj-2uplex  35903  bj-2upln0  35904  bj-2upln1upl  35905