Metamath Proof Explorer


Definition df-cmtN

Description: Define the commutes relation for orthoposets. Definition of commutes in Kalmbach p. 20. (Contributed by NM, 6-Nov-2011)

Ref Expression
Assertion df-cmtN cm=pVxy|xBasepyBasepx=xmeetpyjoinpxmeetpocpy

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmtN classcm
1 vp setvarp
2 cvv classV
3 vx setvarx
4 vy setvary
5 3 cv setvarx
6 cbs classBase
7 1 cv setvarp
8 7 6 cfv classBasep
9 5 8 wcel wffxBasep
10 4 cv setvary
11 10 8 wcel wffyBasep
12 cmee classmeet
13 7 12 cfv classmeetp
14 5 10 13 co classxmeetpy
15 cjn classjoin
16 7 15 cfv classjoinp
17 coc classoc
18 7 17 cfv classocp
19 10 18 cfv classocpy
20 5 19 13 co classxmeetpocpy
21 14 20 16 co classxmeetpyjoinpxmeetpocpy
22 5 21 wceq wffx=xmeetpyjoinpxmeetpocpy
23 9 11 22 w3a wffxBasepyBasepx=xmeetpyjoinpxmeetpocpy
24 23 3 4 copab classxy|xBasepyBasepx=xmeetpyjoinpxmeetpocpy
25 1 2 24 cmpt classpVxy|xBasepyBasepx=xmeetpyjoinpxmeetpocpy
26 0 25 wceq wffcm=pVxy|xBasepyBasepx=xmeetpyjoinpxmeetpocpy