Description: Define the class of poset atoms. (Contributed by NM, 18-Sep-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | df-ats | ⊢ Atoms = ( 𝑝 ∈ V ↦ { 𝑎 ∈ ( Base ‘ 𝑝 ) ∣ ( 0. ‘ 𝑝 ) ( ⋖ ‘ 𝑝 ) 𝑎 } ) |
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. ‘ 𝑝 ) ( ⋖ ‘ 𝑝 ) 𝑎 } ) |