Metamath Proof Explorer


Definition df-bj-2upl

Description: Definition of the Morse couple. See df-bj-1upl . 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-Oct-2018) (New usage is discouraged.)

Ref Expression
Assertion df-bj-2upl A B = A 1 𝑜 × tag B

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cB class B
2 0 1 bj-c2uple class A B
3 0 bj-c1upl class A
4 c1o class 1 𝑜
5 4 csn class 1 𝑜
6 1 bj-ctag class tag B
7 5 6 cxp class 1 𝑜 × tag B
8 3 7 cun class A 1 𝑜 × tag B
9 2 8 wceq wff A B = A 1 𝑜 × tag B