Definition df-bj-1upl

Description: Definition of the Morse monuple (1-tuple). This is not useful per se, but is used as a step towards the definition of couples (2-tuples, or ordered pairs). The reason for "tagging" the set is so that an m-tuple and an n-tuple be equal only when m = n. With this definition, the 0-tuple is the empty set. 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-Apr-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	df-bj-1upl	$$⊢⦅A⦆=\left\{\varnothing \right\}\times tagA$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	bj-c1upl	$$class⦅A⦆$$
2		c0	$$class\varnothing$$
3	2	csn	$$class\left\{\varnothing \right\}$$
4	0	bj-ctag	$$classtagA$$
5	3 4	cxp	$$class\left(\left\{\varnothing \right\}\times tagA\right)$$
6	1 5	wceq	$$wff⦅A⦆=\left\{\varnothing \right\}\times tagA$$