Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-1upl Structured version   Visualization version   Unicode version

Definition df-bj-1upl 31636
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 31650, bj-2uplth 31659, bj-2uplex 31660, and the properties of the projections (see df-bj-pr1 31639 and df-bj-pr2 31653). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
Assertion
Ref Expression
df-bj-1upl  |- (| A|)  =  ( { (/) }  X. tag  A
)

Detailed syntax breakdown of Definition df-bj-1upl
StepHypRef Expression
1 cA . . 3  class  A
21bj-c1upl 31635 . 2  class (| A|)
3 c0 3742 . . . 4  class  (/)
43csn 3979 . . 3  class  { (/) }
51bj-ctag 31612 . . 3  class tag  A
64, 5cxp 4850 . 2  class  ( {
(/) }  X. tag  A )
72, 6wceq 1454 1  wff (| A|)  =  ( { (/) }  X. tag  A
)
Colors of variables: wff setvar class
This definition is referenced by:  bj-1upleq  31637  bj-pr11val  31643  bj-1uplex  31646  bj-1upln0  31647  bj-pr22val  31657  bj-2upln1upl  31662
  Copyright terms: Public domain W3C validator