This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )