df-ats

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

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

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 \in {Base}_{p} \| 0. (p) ⋖_{p} a\}$
14	1 2 13	cmpt	$class (p \in V ⟼ \{a \in {Base}_{p} \| 0. (p) ⋖_{p} a\})$
15	0 14	wceq	$wff Atoms = (p \in V ⟼ \{a \in {Base}_{p} \| 0. (p) ⋖_{p} a\})$

Metamath Proof Explorer