Definition df-bj-2upl 32999

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

Assertion

Ref	Expression
df-bj-2upl	|- (| A, B|) = ((| A|) u. ( { 1o } X. tag B ) )

Detailed syntax breakdown of Definition df-bj-2upl

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	bj-c2uple 32998	. 2 class (| A, B|)
4	1	bj-c1upl 32985	. . 3 class (| A|)
5		c1o 7553	. . . . 5 class 1o
6	5	csn 4177	. . . 4 class { 1o }
7	2	bj-ctag 32962	. . . 4 class tag B
8	6, 7	cxp 5112	. . 3 class ( { 1o } X. tag B )
9	4, 8	cun 3572	. 2 class ((| A|) u. ( { 1o } X. tag B ) )
10	3, 9	wceq 1483	1 wff (| A, B|) = ((| A|) u. ( { 1o } X. tag B ) )

This definition is referenced by:  bj-2upleq  33000  bj-pr21val  33001  bj-pr22val  33007  bj-2uplex  33010  bj-2upln0  33011  bj-2upln1upl  33012