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

Definition df-bj-2upl 31651
Description: Definition of the Morse couple. See df-bj-1upl 31638. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 31652, bj-2uplth 31661, bj-2uplex 31662, and the properties of the projections (see df-bj-pr1 31641 and df-bj-pr2 31655). (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
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2bj-c2uple 31650 . 2  class (| A,  B|)
41bj-c1upl 31637 . . 3  class (| A|)
5 c1o 7206 . . . . 5  class  1o
65csn 3980 . . . 4  class  { 1o }
72bj-ctag 31614 . . . 4  class tag  B
86, 7cxp 4854 . . 3  class  ( { 1o }  X. tag  B
)
94, 8cun 3414 . 2  class  ((| A|)  u.  ( { 1o }  X. tag  B ) )
103, 9wceq 1455 1  wff (| A,  B|)  =  ((| A|)  u.  ( { 1o }  X. tag  B
) )
Colors of variables: wff setvar class
This definition is referenced by:  bj-2upleq  31652  bj-pr21val  31653  bj-pr22val  31659  bj-2uplex  31662  bj-2upln0  31663  bj-2upln1upl  31664
  Copyright terms: Public domain W3C validator