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

Definition df-pmap 28972
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 28965 . 2  class  pmap
2 vk . . 3  set  k
3 cvv 2789 . . 3  class  _V
4 va . . . 4  set  a
52cv 1622 . . . . 5  class  k
6 cbs 13144 . . . . 5  class  Base
75, 6cfv 5221 . . . 4  class  ( Base `  k )
8 vp . . . . . . 7  set  p
98cv 1622 . . . . . 6  class  p
104cv 1622 . . . . . 6  class  a
11 cple 13211 . . . . . . 7  class  le
125, 11cfv 5221 . . . . . 6  class  ( le
`  k )
139, 10, 12wbr 4024 . . . . 5  wff  p ( le `  k ) a
14 catm 28732 . . . . . 6  class  Atoms
155, 14cfv 5221 . . . . 5  class  ( Atoms `  k )
1613, 8, 15crab 2548 . . . 4  class  { p  e.  ( Atoms `  k )  |  p ( le `  k ) a }
174, 7, 16cmpt 4078 . . 3  class  ( a  e.  ( Base `  k
)  |->  { p  e.  ( Atoms `  k )  |  p ( le `  k ) a } )
182, 3, 17cmpt 4078 . 2  class  ( k  e.  _V  |->  ( a  e.  ( Base `  k
)  |->  { p  e.  ( Atoms `  k )  |  p ( le `  k ) a } ) )
191, 18wceq 1623 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  29224
  Copyright terms: Public domain W3C validator