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	$⊢ H \in C_{ℋ}$
	Assertion	pjfoi	$⊢ {proj}_{ℎ} (H) : ℋ \underset{onto}{⟶} H$

Step	Hyp	Ref	Expression
1		pjfn.1	$⊢ H \in C_{ℋ}$
2	1	pjfni	$⊢ {proj}_{ℎ} (H) Fn ℋ$
3	1	pjrni	$⊢ ran {proj}_{ℎ} (H) = H$
4		df-fo	$⊢ {proj}_{ℎ} (H) : ℋ \underset{onto}{⟶} H \leftrightarrow ({proj}_{ℎ} (H) Fn ℋ \land ran {proj}_{ℎ} (H) = H)$
5	2 3 4	mpbir2an	$⊢ {proj}_{ℎ} (H) : ℋ \underset{onto}{⟶} H$