Definition df-ats

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

	Ref	Expression
Assertion	df-ats	⊢ Atoms = ( 𝑝 ∈ V ↦ { 𝑎 ∈ ( Base ‘ 𝑝 ) ∣ ( 0. ‘ 𝑝 ) ( ⋖ ‘ 𝑝 ) 𝑎 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		catm	⊢ Atoms
1		vp	⊢ 𝑝
2		cvv	⊢ V
3		va	⊢ 𝑎
4		cbs	⊢ Base
5	1	cv	⊢ 𝑝
6	5 4	cfv	⊢ ( Base ‘ 𝑝 )
7		cp0	⊢ 0.
8	5 7	cfv	⊢ ( 0. ‘ 𝑝 )
9		ccvr	⊢ ⋖
10	5 9	cfv	⊢ ( ⋖ ‘ 𝑝 )
11	3	cv	⊢ 𝑎
12	8 11 10	wbr	⊢ ( 0. ‘ 𝑝 ) ( ⋖ ‘ 𝑝 ) 𝑎
13	12 3 6	crab	⊢ { 𝑎 ∈ ( Base ‘ 𝑝 ) ∣ ( 0. ‘ 𝑝 ) ( ⋖ ‘ 𝑝 ) 𝑎 }
14	1 2 13	cmpt	⊢ ( 𝑝 ∈ V ↦ { 𝑎 ∈ ( Base ‘ 𝑝 ) ∣ ( 0. ‘ 𝑝 ) ( ⋖ ‘ 𝑝 ) 𝑎 } )
15	0 14	wceq	⊢ Atoms = ( 𝑝 ∈ V ↦ { 𝑎 ∈ ( Base ‘ 𝑝 ) ∣ ( 0. ‘ 𝑝 ) ( ⋖ ‘ 𝑝 ) 𝑎 } )