Metamath Proof Explorer


Theorem pjrn

Description: The range of a projection. Part of Theorem 26.2 of Halmos p. 44. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjrn H C ran proj H = H

Proof

Step Hyp Ref Expression
1 pjhfo H C proj H : onto H
2 forn proj H : onto H ran proj H = H
3 1 2 syl H C ran proj H = H