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

Definition df-ats 30127
Description: Define the class of poset atoms. (Contributed by NM, 18-Sep-2011.)
Assertion
Ref Expression
df-ats  |-  Atoms  =  ( p  e.  _V  |->  { a  e.  ( Base `  p )  |  ( 0. `  p ) (  <o  `  p )
a } )
Distinct variable group:    p, a

Detailed syntax breakdown of Definition df-ats
StepHypRef Expression
1 catm 30123 . 2  class  Atoms
2 vp . . 3  set  p
3 cvv 2958 . . 3  class  _V
42cv 1652 . . . . . 6  class  p
5 cp0 14468 . . . . . 6  class  0.
64, 5cfv 5456 . . . . 5  class  ( 0.
`  p )
7 va . . . . . 6  set  a
87cv 1652 . . . . 5  class  a
9 ccvr 30122 . . . . . 6  class  <o
104, 9cfv 5456 . . . . 5  class  (  <o  `  p )
116, 8, 10wbr 4214 . . . 4  wff  ( 0.
`  p ) ( 
<o  `  p ) a
12 cbs 13471 . . . . 5  class  Base
134, 12cfv 5456 . . . 4  class  ( Base `  p )
1411, 7, 13crab 2711 . . 3  class  { a  e.  ( Base `  p
)  |  ( 0.
`  p ) ( 
<o  `  p ) a }
152, 3, 14cmpt 4268 . 2  class  ( p  e.  _V  |->  { a  e.  ( Base `  p
)  |  ( 0.
`  p ) ( 
<o  `  p ) a } )
161, 15wceq 1653 1  wff  Atoms  =  ( p  e.  _V  |->  { a  e.  ( Base `  p )  |  ( 0. `  p ) (  <o  `  p )
a } )
Colors of variables: wff set class
This definition is referenced by:  pats  30145
  Copyright terms: Public domain W3C validator