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 = ( 𝑝 ∈ 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. ‘ 𝑝 ) ( ⋖ ‘ 𝑝 ) 𝑎 } )