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

Definition df-covers 30078
Description: Define the covers relation ("is covered by") for posets. " a is covered by  b " means that  a is strictly less than  b and there is nothing in between. See cvrval 30081 for the relation form. (Contributed by NM, 18-Sep-2011.)
Assertion
Ref Expression
df-covers  |-  <o  =  ( p  e.  _V  |->  {
<. a ,  b >.  |  ( ( a  e.  ( Base `  p
)  /\  b  e.  ( Base `  p )
)  /\  a ( lt `  p ) b  /\  -.  E. z  e.  ( Base `  p
) ( a ( lt `  p ) z  /\  z ( lt `  p ) b ) ) } )
Distinct variable group:    z, p, a, b

Detailed syntax breakdown of Definition df-covers
StepHypRef Expression
1 ccvr 30074 . 2  class  <o
2 vp . . 3  set  p
3 cvv 2801 . . 3  class  _V
4 va . . . . . . . 8  set  a
54cv 1631 . . . . . . 7  class  a
62cv 1631 . . . . . . . 8  class  p
7 cbs 13164 . . . . . . . 8  class  Base
86, 7cfv 5271 . . . . . . 7  class  ( Base `  p )
95, 8wcel 1696 . . . . . 6  wff  a  e.  ( Base `  p
)
10 vb . . . . . . . 8  set  b
1110cv 1631 . . . . . . 7  class  b
1211, 8wcel 1696 . . . . . 6  wff  b  e.  ( Base `  p
)
139, 12wa 358 . . . . 5  wff  ( a  e.  ( Base `  p
)  /\  b  e.  ( Base `  p )
)
14 cplt 14091 . . . . . . 7  class  lt
156, 14cfv 5271 . . . . . 6  class  ( lt
`  p )
165, 11, 15wbr 4039 . . . . 5  wff  a ( lt `  p ) b
17 vz . . . . . . . . . 10  set  z
1817cv 1631 . . . . . . . . 9  class  z
195, 18, 15wbr 4039 . . . . . . . 8  wff  a ( lt `  p ) z
2018, 11, 15wbr 4039 . . . . . . . 8  wff  z ( lt `  p ) b
2119, 20wa 358 . . . . . . 7  wff  ( a ( lt `  p
) z  /\  z
( lt `  p
) b )
2221, 17, 8wrex 2557 . . . . . 6  wff  E. z  e.  ( Base `  p
) ( a ( lt `  p ) z  /\  z ( lt `  p ) b )
2322wn 3 . . . . 5  wff  -.  E. z  e.  ( Base `  p ) ( a ( lt `  p
) z  /\  z
( lt `  p
) b )
2413, 16, 23w3a 934 . . . 4  wff  ( ( a  e.  ( Base `  p )  /\  b  e.  ( Base `  p
) )  /\  a
( lt `  p
) b  /\  -.  E. z  e.  ( Base `  p ) ( a ( lt `  p
) z  /\  z
( lt `  p
) b ) )
2524, 4, 10copab 4092 . . 3  class  { <. a ,  b >.  |  ( ( a  e.  (
Base `  p )  /\  b  e.  ( Base `  p ) )  /\  a ( lt
`  p ) b  /\  -.  E. z  e.  ( Base `  p
) ( a ( lt `  p ) z  /\  z ( lt `  p ) b ) ) }
262, 3, 25cmpt 4093 . 2  class  ( p  e.  _V  |->  { <. a ,  b >.  |  ( ( a  e.  (
Base `  p )  /\  b  e.  ( Base `  p ) )  /\  a ( lt
`  p ) b  /\  -.  E. z  e.  ( Base `  p
) ( a ( lt `  p ) z  /\  z ( lt `  p ) b ) ) } )
271, 26wceq 1632 1  wff  <o  =  ( p  e.  _V  |->  {
<. a ,  b >.  |  ( ( a  e.  ( Base `  p
)  /\  b  e.  ( Base `  p )
)  /\  a ( lt `  p ) b  /\  -.  E. z  e.  ( Base `  p
) ( a ( lt `  p ) z  /\  z ( lt `  p ) b ) ) } )
Colors of variables: wff set class
This definition is referenced by:  cvrfval  30080
  Copyright terms: Public domain W3C validator