Definition df-cmtN 35354

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 = ( p e. _V |-> { <. x , y >. | ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) ) } )

Distinct variable group:   x, p, y

Detailed syntax breakdown of Definition df-cmtN

Step	Hyp	Ref	Expression
1		ccmtN 35350	. 2 class cm
2		vp	. . 3 setvar p
3		cvv 3051	. . 3 class _V
4		vx	. . . . . . 7 setvar x
5	4	cv 1398	. . . . . 6 class x
6	2	cv 1398	. . . . . . 7 class p
7		cbs 14657	. . . . . . 7 class Base
8	6, 7	cfv 5513	. . . . . 6 class ( Base ` p )
9	5, 8	wcel 1836	. . . . 5 wff x e. ( Base ` p )
10		vy	. . . . . . 7 setvar y
11	10	cv 1398	. . . . . 6 class y
12	11, 8	wcel 1836	. . . . 5 wff y e. ( Base ` p )
13		cmee 15714	. . . . . . . . 9 class meet
14	6, 13	cfv 5513	. . . . . . . 8 class ( meet ` p )
15	5, 11, 14	co 6218	. . . . . . 7 class ( x ( meet ` p ) y )
16		coc 14733	. . . . . . . . . 10 class oc
17	6, 16	cfv 5513	. . . . . . . . 9 class ( oc ` p )
18	11, 17	cfv 5513	. . . . . . . 8 class ( ( oc ` p ) ` y )
19	5, 18, 14	co 6218	. . . . . . 7 class ( x ( meet ` p ) ( ( oc ` p ) ` y ) )
20		cjn 15713	. . . . . . . 8 class join
21	6, 20	cfv 5513	. . . . . . 7 class ( join ` p )
22	15, 19, 21	co 6218	. . . . . 6 class ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) )
23	5, 22	wceq 1399	. . . . 5 wff x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) )
24	9, 12, 23	w3a 971	. . . 4 wff ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) )
25	24, 4, 10	copab 4441	. . 3 class { <. x , y >. | ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) ) }
26	2, 3, 25	cmpt 4442	. 2 class ( p e. _V |-> { <. x , y >. | ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) ) } )
27	1, 26	wceq 1399	1 wff cm = ( p e. _V |-> { <. x , y >. | ( x e. ( Base ` p ) /\ y e. ( Base ` p ) /\ x = ( ( x ( meet ` p ) y ) ( join ` p ) ( x ( meet ` p ) ( ( oc ` p ) ` y ) ) ) ) } )

This definition is referenced by:  cmtfvalN  35387