Metamath Proof Explorer


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. Note that 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 𝐴 ⦆ = ( { ∅ } × tag 𝐴 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 0 bj-c1upl 𝐴
2 c0
3 2 csn { ∅ }
4 0 bj-ctag tag 𝐴
5 3 4 cxp ( { ∅ } × tag 𝐴 )
6 1 5 wceq 𝐴 ⦆ = ( { ∅ } × tag 𝐴 )