Metamath Proof Explorer


Definition df-ats

Description: Define the class of poset atoms. (Contributed by NM, 18-Sep-2011)

Ref Expression
Assertion df-ats Atoms = p V a Base p | 0. p p a

Detailed syntax breakdown

Step Hyp Ref Expression
0 catm class Atoms
1 vp setvar p
2 cvv class V
3 va setvar a
4 cbs class Base
5 1 cv setvar p
6 5 4 cfv class Base p
7 cp0 class 0.
8 5 7 cfv class 0. p
9 ccvr class
10 5 9 cfv class p
11 3 cv setvar a
12 8 11 10 wbr wff 0. p p a
13 12 3 6 crab class a Base p | 0. p p a
14 1 2 13 cmpt class p V a Base p | 0. p p a
15 0 14 wceq wff Atoms = p V a Base p | 0. p p a