Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pmap Structured version   Visualization version   GIF version

Definition df-pmap 37514
Description: Define projective map for 𝑘 at 𝑎. Definition in Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 2-Oct-2011.)
Assertion
Ref Expression
df-pmap pmap = (𝑘 ∈ V ↦ (𝑎 ∈ (Base‘𝑘) ↦ {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎}))
Distinct variable group:   𝑘,𝑎,𝑝

Detailed syntax breakdown of Definition df-pmap
StepHypRef Expression
1 cpmap 37507 . 2 class pmap
2 vk . . 3 setvar 𝑘
3 cvv 3431 . . 3 class V
4 va . . . 4 setvar 𝑎
52cv 1541 . . . . 5 class 𝑘
6 cbs 16910 . . . . 5 class Base
75, 6cfv 6432 . . . 4 class (Base‘𝑘)
8 vp . . . . . . 7 setvar 𝑝
98cv 1541 . . . . . 6 class 𝑝
104cv 1541 . . . . . 6 class 𝑎
11 cple 16967 . . . . . . 7 class le
125, 11cfv 6432 . . . . . 6 class (le‘𝑘)
139, 10, 12wbr 5079 . . . . 5 wff 𝑝(le‘𝑘)𝑎
14 catm 37273 . . . . . 6 class Atoms
155, 14cfv 6432 . . . . 5 class (Atoms‘𝑘)
1613, 8, 15crab 3070 . . . 4 class {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎}
174, 7, 16cmpt 5162 . . 3 class (𝑎 ∈ (Base‘𝑘) ↦ {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎})
182, 3, 17cmpt 5162 . 2 class (𝑘 ∈ V ↦ (𝑎 ∈ (Base‘𝑘) ↦ {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎}))
191, 18wceq 1542 1 wff pmap = (𝑘 ∈ V ↦ (𝑎 ∈ (Base‘𝑘) ↦ {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎}))
Colors of variables: wff setvar class
This definition is referenced by:  pmapfval  37766
  Copyright terms: Public domain W3C validator