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

Metamath Proof Explorer

Theorem pjfoi

Description: A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypothesis pjfn.1 ⊢ 𝐻 ∈ Cℋ
Assertion pjfoi ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻

Proof

Step Hyp Ref Expression
1 pjfn.1 ⊢ 𝐻 ∈ Cℋ
2 1 pjfni ⊢ ( projℎ ‘ 𝐻 ) Fn ℋ
3 1 pjrni ⊢ ran ( projℎ ‘ 𝐻 ) = 𝐻
4 df-fo ⊢ ( ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻 ↔ ( ( projℎ ‘ 𝐻 ) Fn ℋ ∧ ran ( projℎ ‘ 𝐻 ) = 𝐻 ) )
5 2 3 4 mpbir2an ⊢ ( projℎ ‘ 𝐻 ) : ℋ –onto→ 𝐻