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

Definition df-covers 29456
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 29459 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 29452 . 2  class  <o
2 vp . . 3  set  p
3 cvv 2788 . . 3  class  _V
4 va . . . . . . . 8  set  a
54cv 1622 . . . . . . 7  class  a
62cv 1622 . . . . . . . 8  class  p
7 cbs 13148 . . . . . . . 8  class  Base
86, 7cfv 5255 . . . . . . 7  class  ( Base `  p )
95, 8wcel 1684 . . . . . 6  wff  a  e.  ( Base `  p
)
10 vb . . . . . . . 8  set  b
1110cv 1622 . . . . . . 7  class  b
1211, 8wcel 1684 . . . . . 6  wff  b  e.  ( Base `  p
)
139, 12wa 358 . . . . 5  wff  ( a  e.  ( Base `  p
)  /\  b  e.  ( Base `  p )
)
14 cplt 14075 . . . . . . 7  class  lt
156, 14cfv 5255 . . . . . 6  class  ( lt
`  p )
165, 11, 15wbr 4023 . . . . 5  wff  a ( lt `  p ) b
17 vz . . . . . . . . . 10  set  z
1817cv 1622 . . . . . . . . 9  class  z
195, 18, 15wbr 4023 . . . . . . . 8  wff  a ( lt `  p ) z
2018, 11, 15wbr 4023 . . . . . . . 8  wff  z ( lt `  p ) b
2119, 20wa 358 . . . . . . 7  wff  ( a ( lt `  p
) z  /\  z
( lt `  p
) b )
2221, 17, 8wrex 2544 . . . . . 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 4076 . . 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 4077 . 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 1623 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  29458
  Copyright terms: Public domain W3C validator