Definition df-ats

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

	Ref	Expression
Assertion	df-ats	$$⊢\mathrm{Atoms}=\left(p\in \mathrm{V}⟼\left\{a\in {\mathrm{Base}}_p|\mathrm{0.}\left(p\right){⋖}_{p}a\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		catm	$$class\mathrm{Atoms}$$
1		vp	$$setvarp$$
2		cvv	$$class\mathrm{V}$$
3		va	$$setvara$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarp$$
6	5 4	cfv	$$class{\mathrm{Base}}_p$$
7		cp0	$$class\mathrm{0.}$$
8	5 7	cfv	$$class\mathrm{0.}\left(p\right)$$
9		ccvr	$$class⋖$$
10	5 9	cfv	$$class{⋖}_p$$
11	3	cv	$$setvara$$
12	8 11 10	wbr	$$wff\mathrm{0.}\left(p\right){⋖}_{p}a$$
13	12 3 6	crab	$$class\left\{a\in {\mathrm{Base}}_p|\mathrm{0.}\left(p\right){⋖}_{p}a\right\}$$
14	1 2 13	cmpt	$$class\left(p\in \mathrm{V}⟼\left\{a\in {\mathrm{Base}}_p|\mathrm{0.}\left(p\right){⋖}_{p}a\right\}\right)$$
15	0 14	wceq	$$wff\mathrm{Atoms}=\left(p\in \mathrm{V}⟼\left\{a\in {\mathrm{Base}}_p|\mathrm{0.}\left(p\right){⋖}_{p}a\right\}\right)$$