Metamath Proof Explorer


Theorem idiso

Description: The identity is an isomorphism. Example 3.13 of Adamek p. 28. (Contributed by AV, 8-Apr-2020)

Ref Expression
Hypotheses invid.b
|- B = ( Base ` C )
invid.i
|- I = ( Id ` C )
invid.c
|- ( ph -> C e. Cat )
invid.x
|- ( ph -> X e. B )
Assertion idiso
|- ( ph -> ( I ` X ) e. ( X ( Iso ` C ) X ) )

Proof

Step Hyp Ref Expression
1 invid.b
 |-  B = ( Base ` C )
2 invid.i
 |-  I = ( Id ` C )
3 invid.c
 |-  ( ph -> C e. Cat )
4 invid.x
 |-  ( ph -> X e. B )
5 eqid
 |-  ( Inv ` C ) = ( Inv ` C )
6 eqid
 |-  ( Iso ` C ) = ( Iso ` C )
7 1 2 3 4 invid
 |-  ( ph -> ( I ` X ) ( X ( Inv ` C ) X ) ( I ` X ) )
8 1 5 3 4 4 6 7 inviso1
 |-  ( ph -> ( I ` X ) e. ( X ( Iso ` C ) X ) )