Theorem pjhmopidm

Description: Two ways to express the set of all projection operators. (Contributed by NM, 24-Apr-2006) (Proof shortened by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	pjhmopidm	$$⊢\mathrm{ran}{\mathrm{proj}}_{ℎ}=\left\{t\in \mathrm{HrmOp}|t\circ t=t\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfpjop	$$⊢t\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\leftrightarrow \left(t\in \mathrm{HrmOp}\wedge t\circ t=t\right)$$
2	1	eqabi	$$⊢\mathrm{ran}{\mathrm{proj}}_{ℎ}=\left\{t|\left(t\in \mathrm{HrmOp}\wedge t\circ t=t\right)\right\}$$
3		df-rab	$$⊢\left\{t\in \mathrm{HrmOp}|t\circ t=t\right\}=\left\{t|\left(t\in \mathrm{HrmOp}\wedge t\circ t=t\right)\right\}$$
4	2 3	eqtr4i	$$⊢\mathrm{ran}{\mathrm{proj}}_{ℎ}=\left\{t\in \mathrm{HrmOp}|t\circ t=t\right\}$$