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

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 \in C_{ℋ} \to ran {proj}_{ℎ} (H) = H$

Step	Hyp	Ref	Expression
1		pjhfo	$⊢ H \in C_{ℋ} \to {proj}_{ℎ} (H) : ℋ \underset{onto}{⟶} H$
2		forn	$⊢ {proj}_{ℎ} (H) : ℋ \underset{onto}{⟶} H \to ran {proj}_{ℎ} (H) = H$
3	1 2	syl	$⊢ H \in C_{ℋ} \to ran {proj}_{ℎ} (H) = H$