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

Step	Hyp	Ref	Expression
1		pjhfo	$⊢ H \in C_{ℋ} \to {proj}_{ℎ} (H) : ℋ \underset{onto}{⟶} H$
2		fof	$⊢ {proj}_{ℎ} (H) : ℋ \underset{onto}{⟶} H \to {proj}_{ℎ} (H) : ℋ ⟶ H$
3	1 2	syl	$⊢ H \in C_{ℋ} \to {proj}_{ℎ} (H) : ℋ ⟶ H$
4		chss	$⊢ H \in C_{ℋ} \to H \subseteq ℋ$
5	3 4	fssd	$⊢ H \in C_{ℋ} \to {proj}_{ℎ} (H) : ℋ ⟶ ℋ$