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 = ( k e. _V |-> ( a e. ( Base ` k ) |-> { p e. ( Atoms ` k ) | p ( le ` k ) a } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpmap	|- pmap
1		vk	|- k
2		cvv	|- _V
3		va	|- a
4		cbs	|- Base
5	1	cv	|- k
6	5 4	cfv	|- ( Base ` k )
7		vp	|- p
8		catm	|- Atoms
9	5 8	cfv	|- ( Atoms ` k )
10	7	cv	|- p
11		cple	|- le
12	5 11	cfv	|- ( le ` k )
13	3	cv	|- a
14	10 13 12	wbr	|- p ( le ` k ) a
15	14 7 9	crab	|- { p e. ( Atoms ` k ) | p ( le ` k ) a }
16	3 6 15	cmpt	|- ( a e. ( Base ` k ) |-> { p e. ( Atoms ` k ) | p ( le ` k ) a } )
17	1 2 16	cmpt	|- ( k e. _V |-> ( a e. ( Base ` k ) |-> { p e. ( Atoms ` k ) | p ( le ` k ) a } ) )
18	0 17	wceq	|- pmap = ( k e. _V |-> ( a e. ( Base ` k ) |-> { p e. ( Atoms ` k ) | p ( le ` k ) a } ) )