Theorem relcoi1

Description: Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011) (Proof shortened by OpenAI, 3-Jul-2020)

	Ref	Expression
Assertion	relcoi1	⊢ ( Rel 𝑅 → ( 𝑅 ∘ ( I ↾ ∪ ∪ 𝑅 ) ) = 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		coires1	⊢ ( 𝑅 ∘ ( I ↾ ∪ ∪ 𝑅 ) ) = ( 𝑅 ↾ ∪ ∪ 𝑅 )
2		relresfld	⊢ ( Rel 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 )
3	1 2	syl5eq	⊢ ( Rel 𝑅 → ( 𝑅 ∘ ( I ↾ ∪ ∪ 𝑅 ) ) = 𝑅 )