Theorem relcoi2

Description: Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011)

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

Proof

Step	Hyp	Ref	Expression
1		dmrnssfld	⊢ ( dom 𝑅 ∪ ran 𝑅 ) ⊆ ∪ ∪ 𝑅
2		unss	⊢ ( ( dom 𝑅 ⊆ ∪ ∪ 𝑅 ∧ ran 𝑅 ⊆ ∪ ∪ 𝑅 ) ↔ ( dom 𝑅 ∪ ran 𝑅 ) ⊆ ∪ ∪ 𝑅 )
3		simpr	⊢ ( ( dom 𝑅 ⊆ ∪ ∪ 𝑅 ∧ ran 𝑅 ⊆ ∪ ∪ 𝑅 ) → ran 𝑅 ⊆ ∪ ∪ 𝑅 )
4	2 3	sylbir	⊢ ( ( dom 𝑅 ∪ ran 𝑅 ) ⊆ ∪ ∪ 𝑅 → ran 𝑅 ⊆ ∪ ∪ 𝑅 )
5		cores	⊢ ( ran 𝑅 ⊆ ∪ ∪ 𝑅 → ( ( I ↾ ∪ ∪ 𝑅 ) ∘ 𝑅 ) = ( I ∘ 𝑅 ) )
6	1 4 5	mp2b	⊢ ( ( I ↾ ∪ ∪ 𝑅 ) ∘ 𝑅 ) = ( I ∘ 𝑅 )
7		coi2	⊢ ( Rel 𝑅 → ( I ∘ 𝑅 ) = 𝑅 )
8	6 7	eqtrid	⊢ ( Rel 𝑅 → ( ( I ↾ ∪ ∪ 𝑅 ) ∘ 𝑅 ) = 𝑅 )