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

Definition df-pmap 28823
Description: Define projective map for  k at  a. Definition in Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 2-Oct-2011.)
Assertion
Ref Expression
df-pmap  |-  pmap  =  ( k  e.  _V  |->  ( a  e.  (
Base `  k )  |->  { p  e.  (
Atoms `  k )  |  p ( le `  k ) a } ) )
Distinct variable group:    k, a, p

Detailed syntax breakdown of Definition df-pmap
StepHypRef Expression
1 cpmap 28816 . 2  class  pmap
2 vk . . 3  set  k
3 cvv 2740 . . 3  class  _V
4 va . . . 4  set  a
52cv 1618 . . . . 5  class  k
6 cbs 13075 . . . . 5  class  Base
75, 6cfv 4638 . . . 4  class  ( Base `  k )
8 vp . . . . . . 7  set  p
98cv 1618 . . . . . 6  class  p
104cv 1618 . . . . . 6  class  a
11 cple 13142 . . . . . . 7  class  le
125, 11cfv 4638 . . . . . 6  class  ( le
`  k )
139, 10, 12wbr 3963 . . . . 5  wff  p ( le `  k ) a
14 catm 28583 . . . . . 6  class  Atoms
155, 14cfv 4638 . . . . 5  class  ( Atoms `  k )
1613, 8, 15crab 2519 . . . 4  class  { p  e.  ( Atoms `  k )  |  p ( le `  k ) a }
174, 7, 16cmpt 4017 . . 3  class  ( a  e.  ( Base `  k
)  |->  { p  e.  ( Atoms `  k )  |  p ( le `  k ) a } )
182, 3, 17cmpt 4017 . 2  class  ( k  e.  _V  |->  ( a  e.  ( Base `  k
)  |->  { p  e.  ( Atoms `  k )  |  p ( le `  k ) a } ) )
191, 18wceq 1619 1  wff  pmap  =  ( k  e.  _V  |->  ( a  e.  (
Base `  k )  |->  { p  e.  (
Atoms `  k )  |  p ( le `  k ) a } ) )
Colors of variables: wff set class
This definition is referenced by:  pmapfval  29075
  Copyright terms: Public domain W3C validator