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

Definition df-ats 36285
Description: Define the class of poset atoms. (Contributed by NM, 18-Sep-2011.)
Assertion
Ref Expression
df-ats Atoms = (𝑝 ∈ V ↦ {𝑎 ∈ (Base‘𝑝) ∣ (0.‘𝑝)( ⋖ ‘𝑝)𝑎})
Distinct variable group:   𝑝,𝑎

Detailed syntax breakdown of Definition df-ats
StepHypRef Expression
1 catm 36281 . 2 class Atoms
2 vp . . 3 setvar 𝑝
3 cvv 3495 . . 3 class V
42cv 1527 . . . . . 6 class 𝑝
5 cp0 17637 . . . . . 6 class 0.
64, 5cfv 6349 . . . . 5 class (0.‘𝑝)
7 va . . . . . 6 setvar 𝑎
87cv 1527 . . . . 5 class 𝑎
9 ccvr 36280 . . . . . 6 class
104, 9cfv 6349 . . . . 5 class ( ⋖ ‘𝑝)
116, 8, 10wbr 5058 . . . 4 wff (0.‘𝑝)( ⋖ ‘𝑝)𝑎
12 cbs 16473 . . . . 5 class Base
134, 12cfv 6349 . . . 4 class (Base‘𝑝)
1411, 7, 13crab 3142 . . 3 class {𝑎 ∈ (Base‘𝑝) ∣ (0.‘𝑝)( ⋖ ‘𝑝)𝑎}
152, 3, 14cmpt 5138 . 2 class (𝑝 ∈ V ↦ {𝑎 ∈ (Base‘𝑝) ∣ (0.‘𝑝)( ⋖ ‘𝑝)𝑎})
161, 15wceq 1528 1 wff Atoms = (𝑝 ∈ V ↦ {𝑎 ∈ (Base‘𝑝) ∣ (0.‘𝑝)( ⋖ ‘𝑝)𝑎})
Colors of variables: wff setvar class
This definition is referenced by:  pats  36303
  Copyright terms: Public domain W3C validator