Metamath Proof Explorer


Theorem pjfi

Description: The mapping of a projection. (Contributed by NM, 11-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypothesis pjfn.1 HC
Assertion pjfi projH:

Proof

Step Hyp Ref Expression
1 pjfn.1 HC
2 1 pjfni projHFn
3 1 pjrni ranprojH=H
4 1 chssii H
5 3 4 eqsstri ranprojH
6 df-f projH:projHFnranprojH
7 2 5 6 mpbir2an projH: