Metamath Proof Explorer

Theorem coi2

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 coi2 
|- ( Rel A -> ( _I o. A ) = A )

Proof

Step Hyp Ref Expression
1 dfrel2 
 |-  ( Rel A <-> `' `' A = A )
2 cnvco 
 |-  `' ( `' A o. _I ) = ( `' _I o. `' `' A )
3 relcnv 
 |-  Rel `' A
4 coi1 
 |-  ( Rel `' A -> ( `' A o. _I ) = `' A )
5 3 4 ax-mp 
 |-  ( `' A o. _I ) = `' A
6 5 cnveqi 
 |-  `' ( `' A o. _I ) = `' `' A
7 2 6 eqtr3i 
 |-  ( `' _I o. `' `' A ) = `' `' A
8 cnvi 
 |-  `' _I = _I
9 coeq2 
 |-  ( `' `' A = A -> ( `' _I o. `' `' A ) = ( `' _I o. A ) )
10 coeq1 
 |-  ( `' _I = _I -> ( `' _I o. A ) = ( _I o. A ) )
11 9 10 sylan9eq 
 |-  ( ( `' `' A = A /\ `' _I = _I ) -> ( `' _I o. `' `' A ) = ( _I o. A ) )
12 8 11 mpan2 
 |-  ( `' `' A = A -> ( `' _I o. `' `' A ) = ( _I o. A ) )
13 id 
 |-  ( `' `' A = A -> `' `' A = A )
14 7 12 13 3eqtr3a 
 |-  ( `' `' A = A -> ( _I o. A ) = A )
15 1 14 sylbi 
 |-  ( Rel A -> ( _I o. A ) = A )