Metamath Proof Explorer


Theorem pjhf

Description: The mapping of a projection. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjhf HCprojH:

Proof

Step Hyp Ref Expression
1 pjhfo HCprojH:ontoH
2 fof projH:ontoHprojH:H
3 1 2 syl HCprojH:H
4 chss HCH
5 3 4 fssd HCprojH: