Definition df-cmtN 37191

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 37187	. 2 class cm
2		vp	. . 3 setvar 𝑝
3		cvv 3432	. . 3 class V
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1538	. . . . . 6 class 𝑥
6	2	cv 1538	. . . . . . 7 class 𝑝
7		cbs 16912	. . . . . . 7 class Base
8	6, 7	cfv 6433	. . . . . 6 class (Base‘𝑝)
9	5, 8	wcel 2106	. . . . 5 wff 𝑥 ∈ (Base‘𝑝)
10		vy	. . . . . . 7 setvar 𝑦
11	10	cv 1538	. . . . . 6 class 𝑦
12	11, 8	wcel 2106	. . . . 5 wff 𝑦 ∈ (Base‘𝑝)
13		cmee 18030	. . . . . . . . 9 class meet
14	6, 13	cfv 6433	. . . . . . . 8 class (meet‘𝑝)
15	5, 11, 14	co 7275	. . . . . . 7 class (𝑥(meet‘𝑝)𝑦)
16		coc 16970	. . . . . . . . . 10 class oc
17	6, 16	cfv 6433	. . . . . . . . 9 class (oc‘𝑝)
18	11, 17	cfv 6433	. . . . . . . 8 class ((oc‘𝑝)‘𝑦)
19	5, 18, 14	co 7275	. . . . . . 7 class (𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))
20		cjn 18029	. . . . . . . 8 class join
21	6, 20	cfv 6433	. . . . . . 7 class (join‘𝑝)
22	15, 19, 21	co 7275	. . . . . 6 class ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦)))
23	5, 22	wceq 1539	. . . . 5 wff 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦)))
24	9, 12, 23	w3a 1086	. . . 4 wff (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))
25	24, 4, 10	copab 5136	. . 3 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))}
26	2, 3, 25	cmpt 5157	. 2 class (𝑝 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))})
27	1, 26	wceq 1539	1 wff cm = (𝑝 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))})

This definition is referenced by:  cmtfvalN  37224