Theorem pjidmcoi

Description: A projection is idempotent. Property (ii) of Beran p. 109. (Contributed by NM, 1-Oct-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjidmco.1	|- H e. CH
Assertion	pjidmcoi	|- ( ( projh ` H ) o. ( projh ` H ) ) = ( projh ` H )

Proof

Step	Hyp	Ref	Expression
1		pjidmco.1	|- H e. CH
2		ssid	|- H C_ H
3	1 1	pjss2coi	|- ( H C_ H <-> ( ( projh ` H ) o. ( projh ` H ) ) = ( projh ` H ) )
4	2 3	mpbi	|- ( ( projh ` H ) o. ( projh ` H ) ) = ( projh ` H )