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

Definition df-bj-2upl 32192
Description: Definition of the Morse couple. See df-bj-1upl 32179. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 32193, bj-2uplth 32202, bj-2uplex 32203, and the properties of the projections (see df-bj-pr1 32182 and df-bj-pr2 32196). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
Assertion
Ref Expression
df-bj-2upl 𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1𝑜} × tag 𝐵))

Detailed syntax breakdown of Definition df-bj-2upl
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2bj-c2uple 32191 . 2 class 𝐴, 𝐵
41bj-c1upl 32178 . . 3 class 𝐴
5 c1o 7440 . . . . 5 class 1𝑜
65csn 4125 . . . 4 class {1𝑜}
72bj-ctag 32155 . . . 4 class tag 𝐵
86, 7cxp 5036 . . 3 class ({1𝑜} × tag 𝐵)
94, 8cun 3538 . 2 class (⦅𝐴⦆ ∪ ({1𝑜} × tag 𝐵))
103, 9wceq 1475 1 wff 𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1𝑜} × tag 𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  bj-2upleq  32193  bj-pr21val  32194  bj-pr22val  32200  bj-2uplex  32203  bj-2upln0  32204  bj-2upln1upl  32205
  Copyright terms: Public domain W3C validator