Definition df-pmap 38842

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 38835	. 2 class pmap
2		vk	. . 3 setvar 𝑘
3		cvv 3473	. . 3 class V
4		va	. . . 4 setvar 𝑎
5	2	cv 1539	. . . . 5 class 𝑘
6		cbs 17151	. . . . 5 class Base
7	5, 6	cfv 6543	. . . 4 class (Base‘𝑘)
8		vp	. . . . . . 7 setvar 𝑝
9	8	cv 1539	. . . . . 6 class 𝑝
10	4	cv 1539	. . . . . 6 class 𝑎
11		cple 17211	. . . . . . 7 class le
12	5, 11	cfv 6543	. . . . . 6 class (le‘𝑘)
13	9, 10, 12	wbr 5148	. . . . 5 wff 𝑝(le‘𝑘)𝑎
14		catm 38600	. . . . . 6 class Atoms
15	5, 14	cfv 6543	. . . . 5 class (Atoms‘𝑘)
16	13, 8, 15	crab 3431	. . . 4 class {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎}
17	4, 7, 16	cmpt 5231	. . 3 class (𝑎 ∈ (Base‘𝑘) ↦ {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎})
18	2, 3, 17	cmpt 5231	. 2 class (𝑘 ∈ V ↦ (𝑎 ∈ (Base‘𝑘) ↦ {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎}))
19	1, 18	wceq 1540	1 wff pmap = (𝑘 ∈ V ↦ (𝑎 ∈ (Base‘𝑘) ↦ {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)𝑎}))

This definition is referenced by:  pmapfval  39094