relcoi2

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

		Ref	Expression
	Assertion	relcoi2	$⊢ Rel R \to ({I ↾}_{⋃ ⋃ R}) \circ R = R$

Step	Hyp	Ref	Expression
1		dmrnssfld	$⊢ dom R \cup ran R \subseteq ⋃ ⋃ R$
2		unss	$⊢ (dom R \subseteq ⋃ ⋃ R \land ran R \subseteq ⋃ ⋃ R) \leftrightarrow dom R \cup ran R \subseteq ⋃ ⋃ R$
3		simpr	$⊢ (dom R \subseteq ⋃ ⋃ R \land ran R \subseteq ⋃ ⋃ R) \to ran R \subseteq ⋃ ⋃ R$
4	2 3	sylbir	$⊢ dom R \cup ran R \subseteq ⋃ ⋃ R \to ran R \subseteq ⋃ ⋃ R$
5		cores	$⊢ ran R \subseteq ⋃ ⋃ R \to ({I ↾}_{⋃ ⋃ R}) \circ R = I \circ R$
6	1 4 5	mp2b	$⊢ ({I ↾}_{⋃ ⋃ R}) \circ R = I \circ R$
7		coi2	$⊢ Rel R \to I \circ R = R$
8	6 7	eqtrid	$⊢ Rel R \to ({I ↾}_{⋃ ⋃ R}) \circ R = R$

Metamath Proof Explorer