Description: Functionality of a projection. (Contributed by NM, 30-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | pjfn.1 | |- H e. CH |
|
| Assertion | pjfni | |- ( projh ` H ) Fn ~H |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pjfn.1 | |- H e. CH |
|
| 2 | riotaex | |- ( iota_ y e. H E. z e. ( _|_ ` H ) x = ( y +h z ) ) e. _V |
|
| 3 | pjhfval | |- ( H e. CH -> ( projh ` H ) = ( x e. ~H |-> ( iota_ y e. H E. z e. ( _|_ ` H ) x = ( y +h z ) ) ) ) |
|
| 4 | 1 3 | ax-mp | |- ( projh ` H ) = ( x e. ~H |-> ( iota_ y e. H E. z e. ( _|_ ` H ) x = ( y +h z ) ) ) |
| 5 | 2 4 | fnmpti | |- ( projh ` H ) Fn ~H |