Theorem relexp0

Description: A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020)

	Ref	Expression
Assertion	relexp0	|- ( ( R e. V /\ Rel R ) -> ( R ^r 0 ) = ( _I |` U. U. R ) )

Proof

Step	Hyp	Ref	Expression
1		relexp0g	|- ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
2		relfld	|- ( Rel R -> U. U. R = ( dom R u. ran R ) )
3	2	reseq2d	|- ( Rel R -> ( _I |` U. U. R ) = ( _I |` ( dom R u. ran R ) ) )
4	3	eqcomd	|- ( Rel R -> ( _I |` ( dom R u. ran R ) ) = ( _I |` U. U. R ) )
5	1 4	sylan9eq	|- ( ( R e. V /\ Rel R ) -> ( R ^r 0 ) = ( _I |` U. U. R ) )