# 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 ${⊢}\mathrm{cm}=\left({p}\in \mathrm{V}⟼\left\{⟨{x},{y}⟩|\left({x}\in {\mathrm{Base}}_{{p}}\wedge {y}\in {\mathrm{Base}}_{{p}}\wedge {x}=\left({x}\mathrm{meet}\left({p}\right){y}\right)\mathrm{join}\left({p}\right)\left({x}\mathrm{meet}\left({p}\right)\mathrm{oc}\left({p}\right)\left({y}\right)\right)\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmtN ${class}\mathrm{cm}$
1 vp ${setvar}{p}$
2 cvv ${class}\mathrm{V}$
3 vx ${setvar}{x}$
4 vy ${setvar}{y}$
5 3 cv ${setvar}{x}$
6 cbs ${class}\mathrm{Base}$
7 1 cv ${setvar}{p}$
8 7 6 cfv ${class}{\mathrm{Base}}_{{p}}$
9 5 8 wcel ${wff}{x}\in {\mathrm{Base}}_{{p}}$
10 4 cv ${setvar}{y}$
11 10 8 wcel ${wff}{y}\in {\mathrm{Base}}_{{p}}$
12 cmee ${class}\mathrm{meet}$
13 7 12 cfv ${class}\mathrm{meet}\left({p}\right)$
14 5 10 13 co ${class}\left({x}\mathrm{meet}\left({p}\right){y}\right)$
15 cjn ${class}\mathrm{join}$
16 7 15 cfv ${class}\mathrm{join}\left({p}\right)$
17 coc ${class}\mathrm{oc}$
18 7 17 cfv ${class}\mathrm{oc}\left({p}\right)$
19 10 18 cfv ${class}\mathrm{oc}\left({p}\right)\left({y}\right)$
20 5 19 13 co ${class}\left({x}\mathrm{meet}\left({p}\right)\mathrm{oc}\left({p}\right)\left({y}\right)\right)$
21 14 20 16 co ${class}\left(\left({x}\mathrm{meet}\left({p}\right){y}\right)\mathrm{join}\left({p}\right)\left({x}\mathrm{meet}\left({p}\right)\mathrm{oc}\left({p}\right)\left({y}\right)\right)\right)$
22 5 21 wceq ${wff}{x}=\left({x}\mathrm{meet}\left({p}\right){y}\right)\mathrm{join}\left({p}\right)\left({x}\mathrm{meet}\left({p}\right)\mathrm{oc}\left({p}\right)\left({y}\right)\right)$
23 9 11 22 w3a ${wff}\left({x}\in {\mathrm{Base}}_{{p}}\wedge {y}\in {\mathrm{Base}}_{{p}}\wedge {x}=\left({x}\mathrm{meet}\left({p}\right){y}\right)\mathrm{join}\left({p}\right)\left({x}\mathrm{meet}\left({p}\right)\mathrm{oc}\left({p}\right)\left({y}\right)\right)\right)$
24 23 3 4 copab ${class}\left\{⟨{x},{y}⟩|\left({x}\in {\mathrm{Base}}_{{p}}\wedge {y}\in {\mathrm{Base}}_{{p}}\wedge {x}=\left({x}\mathrm{meet}\left({p}\right){y}\right)\mathrm{join}\left({p}\right)\left({x}\mathrm{meet}\left({p}\right)\mathrm{oc}\left({p}\right)\left({y}\right)\right)\right)\right\}$
25 1 2 24 cmpt ${class}\left({p}\in \mathrm{V}⟼\left\{⟨{x},{y}⟩|\left({x}\in {\mathrm{Base}}_{{p}}\wedge {y}\in {\mathrm{Base}}_{{p}}\wedge {x}=\left({x}\mathrm{meet}\left({p}\right){y}\right)\mathrm{join}\left({p}\right)\left({x}\mathrm{meet}\left({p}\right)\mathrm{oc}\left({p}\right)\left({y}\right)\right)\right)\right\}\right)$
26 0 25 wceq ${wff}\mathrm{cm}=\left({p}\in \mathrm{V}⟼\left\{⟨{x},{y}⟩|\left({x}\in {\mathrm{Base}}_{{p}}\wedge {y}\in {\mathrm{Base}}_{{p}}\wedge {x}=\left({x}\mathrm{meet}\left({p}\right){y}\right)\mathrm{join}\left({p}\right)\left({x}\mathrm{meet}\left({p}\right)\mathrm{oc}\left({p}\right)\left({y}\right)\right)\right)\right\}\right)$