Definition df-ats

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

	Ref	Expression
Assertion	df-ats	|- Atoms = ( p e. _V |-> { a e. ( Base ` p ) | ( 0. ` p ) (

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		catm	|- Atoms
1		vp	|- p
2		cvv	|- _V
3		va	|- a
4		cbs	|- Base
5	1	cv	|- p
6	5 4	cfv	|- ( Base ` p )
7		cp0	|- 0.
8	5 7	cfv	|- ( 0. ` p )
9		ccvr	|-
10	5 9	cfv	|- (
11	3	cv	|- a
12	8 11 10	wbr	|- ( 0. ` p ) (
13	12 3 6	crab	|- { a e. ( Base ` p ) | ( 0. ` p ) (
14	1 2 13	cmpt	|- ( p e. _V |-> { a e. ( Base ` p ) | ( 0. ` p ) (
15	0 14	wceq	|- Atoms = ( p e. _V |-> { a e. ( Base ` p ) | ( 0. ` p ) (