Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cmtN Structured version   Visualization version   GIF version

Definition df-cmtN 33941
Description: Define the commutes relation for orthoposets. Definition of commutes in [Kalmbach] p. 20. (Contributed by NM, 6-Nov-2011.)
Assertion
Ref Expression
df-cmtN cm = (𝑝 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))})
Distinct variable group:   𝑥,𝑝,𝑦

Detailed syntax breakdown of Definition df-cmtN
StepHypRef Expression
1 ccmtN 33937 . 2 class cm
2 vp . . 3 setvar 𝑝
3 cvv 3186 . . 3 class V
4 vx . . . . . . 7 setvar 𝑥
54cv 1479 . . . . . 6 class 𝑥
62cv 1479 . . . . . . 7 class 𝑝
7 cbs 15781 . . . . . . 7 class Base
86, 7cfv 5847 . . . . . 6 class (Base‘𝑝)
95, 8wcel 1987 . . . . 5 wff 𝑥 ∈ (Base‘𝑝)
10 vy . . . . . . 7 setvar 𝑦
1110cv 1479 . . . . . 6 class 𝑦
1211, 8wcel 1987 . . . . 5 wff 𝑦 ∈ (Base‘𝑝)
13 cmee 16866 . . . . . . . . 9 class meet
146, 13cfv 5847 . . . . . . . 8 class (meet‘𝑝)
155, 11, 14co 6604 . . . . . . 7 class (𝑥(meet‘𝑝)𝑦)
16 coc 15870 . . . . . . . . . 10 class oc
176, 16cfv 5847 . . . . . . . . 9 class (oc‘𝑝)
1811, 17cfv 5847 . . . . . . . 8 class ((oc‘𝑝)‘𝑦)
195, 18, 14co 6604 . . . . . . 7 class (𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))
20 cjn 16865 . . . . . . . 8 class join
216, 20cfv 5847 . . . . . . 7 class (join‘𝑝)
2215, 19, 21co 6604 . . . . . 6 class ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦)))
235, 22wceq 1480 . . . . 5 wff 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦)))
249, 12, 23w3a 1036 . . . 4 wff (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))
2524, 4, 10copab 4672 . . 3 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))}
262, 3, 25cmpt 4673 . 2 class (𝑝 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))})
271, 26wceq 1480 1 wff cm = (𝑝 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))})
Colors of variables: wff setvar class
This definition is referenced by:  cmtfvalN  33974
  Copyright terms: Public domain W3C validator