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 = p ∈ V ⟼ x y | x ∈ Base p ∧ y ∈ Base p ∧ x = x meet ⁡ p y join ⁡ p x meet ⁡ p oc ⁡ p ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmtN class cm
1 vp setvar p
2 cvv class V
3 vx setvar x
4 vy setvar y
5 3 cv setvar x
6 cbs class Base
7 1 cv setvar p
8 7 6 cfv class Base p
9 5 8 wcel wff x ∈ Base p
10 4 cv setvar y
11 10 8 wcel wff y ∈ Base p
12 cmee class meet
13 7 12 cfv class meet ⁡ p
14 5 10 13 co class x meet ⁡ p y
15 cjn class join
16 7 15 cfv class join ⁡ p
17 coc class oc
18 7 17 cfv class oc ⁡ p
19 10 18 cfv class oc ⁡ p ⁡ y
20 5 19 13 co class x meet ⁡ p oc ⁡ p ⁡ y
21 14 20 16 co class x meet ⁡ p y join ⁡ p x meet ⁡ p oc ⁡ p ⁡ y
22 5 21 wceq wff x = x meet ⁡ p y join ⁡ p x meet ⁡ p oc ⁡ p ⁡ y
23 9 11 22 w3a wff x ∈ Base p ∧ y ∈ Base p ∧ x = x meet ⁡ p y join ⁡ p x meet ⁡ p oc ⁡ p ⁡ y
24 23 3 4 copab class x y | x ∈ Base p ∧ y ∈ Base p ∧ x = x meet ⁡ p y join ⁡ p x meet ⁡ p oc ⁡ p ⁡ y
25 1 2 24 cmpt class p ∈ V ⟼ x y | x ∈ Base p ∧ y ∈ Base p ∧ x = x meet ⁡ p y join ⁡ p x meet ⁡ p oc ⁡ p ⁡ y
26 0 25 wceq wff cm = p ∈ V ⟼ x y | x ∈ Base p ∧ y ∈ Base p ∧ x = x meet ⁡ p y join ⁡ p x meet ⁡ p oc ⁡ p ⁡ y