Definition df-pmap

Description: Define projective map for k at a . Definition in Theorem 15.5 of MaedaMaeda p. 62. (Contributed by NM, 2-Oct-2011)

	Ref	Expression
Assertion	df-pmap	⊢ pmap = ( 𝑘 ∈ V ↦ ( 𝑎 ∈ ( Base ‘ 𝑘 ) ↦ { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) 𝑎 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpmap	⊢ pmap
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		va	⊢ 𝑎
4		cbs	⊢ Base
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( Base ‘ 𝑘 )
7		vp	⊢ 𝑝
8		catm	⊢ Atoms
9	5 8	cfv	⊢ ( Atoms ‘ 𝑘 )
10	7	cv	⊢ 𝑝
11		cple	⊢ le
12	5 11	cfv	⊢ ( le ‘ 𝑘 )
13	3	cv	⊢ 𝑎
14	10 13 12	wbr	⊢ 𝑝 ( le ‘ 𝑘 ) 𝑎
15	14 7 9	crab	⊢ { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) 𝑎 }
16	3 6 15	cmpt	⊢ ( 𝑎 ∈ ( Base ‘ 𝑘 ) ↦ { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) 𝑎 } )
17	1 2 16	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑎 ∈ ( Base ‘ 𝑘 ) ↦ { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) 𝑎 } ) )
18	0 17	wceq	⊢ pmap = ( 𝑘 ∈ V ↦ ( 𝑎 ∈ ( Base ‘ 𝑘 ) ↦ { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) 𝑎 } ) )