This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ )

Proof

Step Hyp Ref Expression
1 pjhfo ⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻 )
2 fof ⊢ ( ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻 → ( projℎ ‘ 𝐻 ) : ℋ ⟶ 𝐻 )
3 1 2 syl ⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) : ℋ ⟶ 𝐻 )
4 chss ⊢ ( 𝐻 ∈ Cℋ → 𝐻 ⊆ ℋ )
5 3 4 fssd ⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ )