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

Definition df-cmtN 29367
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
StepHypRef Expression
1 ccmtN 29363 . 2  class  cm
2 vp . . 3  set  p
3 cvv 2788 . . 3  class  _V
4 vx . . . . . . 7  set  x
54cv 1622 . . . . . 6  class  x
62cv 1622 . . . . . . 7  class  p
7 cbs 13148 . . . . . . 7  class  Base
86, 7cfv 5255 . . . . . 6  class  ( Base `  p )
95, 8wcel 1684 . . . . 5  wff  x  e.  ( Base `  p
)
10 vy . . . . . . 7  set  y
1110cv 1622 . . . . . 6  class  y
1211, 8wcel 1684 . . . . 5  wff  y  e.  ( Base `  p
)
13 cmee 14079 . . . . . . . . 9  class  meet
146, 13cfv 5255 . . . . . . . 8  class  ( meet `  p )
155, 11, 14co 5858 . . . . . . 7  class  ( x ( meet `  p
) y )
16 coc 13216 . . . . . . . . . 10  class  oc
176, 16cfv 5255 . . . . . . . . 9  class  ( oc
`  p )
1811, 17cfv 5255 . . . . . . . 8  class  ( ( oc `  p ) `
 y )
195, 18, 14co 5858 . . . . . . 7  class  ( x ( meet `  p
) ( ( oc
`  p ) `  y ) )
20 cjn 14078 . . . . . . . 8  class  join
216, 20cfv 5255 . . . . . . 7  class  ( join `  p )
2215, 19, 21co 5858 . . . . . 6  class  ( ( x ( meet `  p
) y ) (
join `  p )
( x ( meet `  p ) ( ( oc `  p ) `
 y ) ) )
235, 22wceq 1623 . . . . 5  wff  x  =  ( ( x (
meet `  p )
y ) ( join `  p ) ( x ( meet `  p
) ( ( oc
`  p ) `  y ) ) )
249, 12, 23w3a 934 . . . 4  wff  ( x  e.  ( Base `  p
)  /\  y  e.  ( Base `  p )  /\  x  =  (
( x ( meet `  p ) y ) ( join `  p
) ( x (
meet `  p )
( ( oc `  p ) `  y
) ) ) )
2524, 4, 10copab 4076 . . 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 ) ) ) ) }
262, 3, 25cmpt 4077 . 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 ) ) ) ) } )
271, 26wceq 1623 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
) ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  cmtfvalN  29400
  Copyright terms: Public domain W3C validator