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 H C proj H :

Proof

Step Hyp Ref Expression
1 pjhfo H C proj H : onto H
2 fof proj H : onto H proj H : H
3 1 2 syl H C proj H : H
4 chss H C H
5 3 4 fssd H C proj H :