Theorem coi1

Description: Composition with the identity relation. Part of Theorem 3.7(i) of Monk1 p. 36. (Contributed by NM, 22-Apr-2004)

	Ref	Expression
Assertion	coi1	|- ( Rel A -> ( A o. _I ) = A )

Proof

Step	Hyp	Ref	Expression
1		relco	|- Rel ( A o. _I )
2		vex	|- x e. _V
3		vex	|- y e. _V
4	2 3	opelco	|- ( <. x , y >. e. ( A o. _I ) <-> E. z ( x _I z /\ z A y ) )
5		vex	|- z e. _V
6	5	ideq	|- ( x _I z <-> x = z )
7		equcom	|- ( x = z <-> z = x )
8	6 7	bitri	|- ( x _I z <-> z = x )
9	8	anbi1i	|- ( ( x _I z /\ z A y ) <-> ( z = x /\ z A y ) )
10	9	exbii	|- ( E. z ( x _I z /\ z A y ) <-> E. z ( z = x /\ z A y ) )
11		breq1	|- ( z = x -> ( z A y <-> x A y ) )
12	11	equsexvw	|- ( E. z ( z = x /\ z A y ) <-> x A y )
13	10 12	bitri	|- ( E. z ( x _I z /\ z A y ) <-> x A y )
14	4 13	bitri	|- ( <. x , y >. e. ( A o. _I ) <-> x A y )
15		df-br	|- ( x A y <-> <. x , y >. e. A )
16	14 15	bitri	|- ( <. x , y >. e. ( A o. _I ) <-> <. x , y >. e. A )
17	16	eqrelriv	|- ( ( Rel ( A o. _I ) /\ Rel A ) -> ( A o. _I ) = A )
18	1 17	mpan	|- ( Rel A -> ( A o. _I ) = A )