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	|- ran projh = { t e. HrmOp | ( t o. t ) = t }

Proof

Step	Hyp	Ref	Expression
1		dfpjop	|- ( t e. ran projh <-> ( t e. HrmOp /\ ( t o. t ) = t ) )
2	1	abbi2i	|- ran projh = { t | ( t e. HrmOp /\ ( t o. t ) = t ) }
3		df-rab	|- { t e. HrmOp | ( t o. t ) = t } = { t | ( t e. HrmOp /\ ( t o. t ) = t ) }
4	2 3	eqtr4i	|- ran projh = { t e. HrmOp | ( t o. t ) = t }