Definition df-cmtN 38036

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

Step	Hyp	Ref	Expression
1		ccmtN 38032	. 2 class cm
2		vp	. . 3 setvar 𝑝
3		cvv 3475	. . 3 class V
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1541	. . . . . 6 class 𝑥
6	2	cv 1541	. . . . . . 7 class 𝑝
7		cbs 17141	. . . . . . 7 class Base
8	6, 7	cfv 6541	. . . . . 6 class (Base‘𝑝)
9	5, 8	wcel 2107	. . . . 5 wff 𝑥 ∈ (Base‘𝑝)
10		vy	. . . . . . 7 setvar 𝑦
11	10	cv 1541	. . . . . 6 class 𝑦
12	11, 8	wcel 2107	. . . . 5 wff 𝑦 ∈ (Base‘𝑝)
13		cmee 18262	. . . . . . . . 9 class meet
14	6, 13	cfv 6541	. . . . . . . 8 class (meet‘𝑝)
15	5, 11, 14	co 7406	. . . . . . 7 class (𝑥(meet‘𝑝)𝑦)
16		coc 17202	. . . . . . . . . 10 class oc
17	6, 16	cfv 6541	. . . . . . . . 9 class (oc‘𝑝)
18	11, 17	cfv 6541	. . . . . . . 8 class ((oc‘𝑝)‘𝑦)
19	5, 18, 14	co 7406	. . . . . . 7 class (𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))
20		cjn 18261	. . . . . . . 8 class join
21	6, 20	cfv 6541	. . . . . . 7 class (join‘𝑝)
22	15, 19, 21	co 7406	. . . . . 6 class ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦)))
23	5, 22	wceq 1542	. . . . 5 wff 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦)))
24	9, 12, 23	w3a 1088	. . . 4 wff (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))
25	24, 4, 10	copab 5210	. . 3 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))}
26	2, 3, 25	cmpt 5231	. 2 class (𝑝 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))})
27	1, 26	wceq 1542	1 wff cm = (𝑝 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))})

This definition is referenced by:  cmtfvalN  38069