Definition df-pmap 39506

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

Step	Hyp	Ref	Expression
1		cpmap 39499	. 2 class pmap
2		vk	. . 3 setvar 𝑘
3		cvv 3480	. . 3 class V
4		va	. . . 4 setvar 𝑎
5	2	cv 1539	. . . . 5 class 𝑘
6		cbs 17247	. . . . 5 class Base
7	5, 6	cfv 6561	. . . 4 class (Base‘𝑘)
8		vp	. . . . . . 7 setvar 𝑝
9	8	cv 1539	. . . . . 6 class 𝑝
10	4	cv 1539	. . . . . 6 class 𝑎
11		cple 17304	. . . . . . 7 class le
12	5, 11	cfv 6561	. . . . . 6 class (le‘𝑘)
13	9, 10, 12	wbr 5143	. . . . 5 wff 𝑝(le‘𝑘)𝑎
14		catm 39264	. . . . . 6 class Atoms
15	5, 14	cfv 6561	. . . . 5 class (Atoms‘𝑘)
16	13, 8, 15	crab 3436	. . . 4 class {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎}
17	4, 7, 16	cmpt 5225	. . 3 class (𝑎 ∈ (Base‘𝑘) ↦ {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎})
18	2, 3, 17	cmpt 5225	. 2 class (𝑘 ∈ V ↦ (𝑎 ∈ (Base‘𝑘) ↦ {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎}))
19	1, 18	wceq 1540	1 wff pmap = (𝑘 ∈ V ↦ (𝑎 ∈ (Base‘𝑘) ↦ {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎}))

This definition is referenced by:  pmapfval  39758