# Metamath Proof Explorer

## Theorem cidval

Description: Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses cidfval.b
`|- B = ( Base ` C )`
cidfval.h
`|- H = ( Hom ` C )`
cidfval.o
`|- .x. = ( comp ` C )`
cidfval.c
`|- ( ph -> C e. Cat )`
cidfval.i
`|- .1. = ( Id ` C )`
cidval.x
`|- ( ph -> X e. B )`
Assertion cidval
`|- ( ph -> ( .1. ` X ) = ( iota_ g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) ) )`

### Proof

Step Hyp Ref Expression
1 cidfval.b
` |-  B = ( Base ` C )`
2 cidfval.h
` |-  H = ( Hom ` C )`
3 cidfval.o
` |-  .x. = ( comp ` C )`
4 cidfval.c
` |-  ( ph -> C e. Cat )`
5 cidfval.i
` |-  .1. = ( Id ` C )`
6 cidval.x
` |-  ( ph -> X e. B )`
7 1 2 3 4 5 cidfval
` |-  ( ph -> .1. = ( x e. B |-> ( iota_ g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) ) ) )`
8 simpr
` |-  ( ( ph /\ x = X ) -> x = X )`
9 8 8 oveq12d
` |-  ( ( ph /\ x = X ) -> ( x H x ) = ( X H X ) )`
10 8 oveq2d
` |-  ( ( ph /\ x = X ) -> ( y H x ) = ( y H X ) )`
11 8 opeq2d
` |-  ( ( ph /\ x = X ) -> <. y , x >. = <. y , X >. )`
12 11 8 oveq12d
` |-  ( ( ph /\ x = X ) -> ( <. y , x >. .x. x ) = ( <. y , X >. .x. X ) )`
13 12 oveqd
` |-  ( ( ph /\ x = X ) -> ( g ( <. y , x >. .x. x ) f ) = ( g ( <. y , X >. .x. X ) f ) )`
14 13 eqeq1d
` |-  ( ( ph /\ x = X ) -> ( ( g ( <. y , x >. .x. x ) f ) = f <-> ( g ( <. y , X >. .x. X ) f ) = f ) )`
15 10 14 raleqbidv
` |-  ( ( ph /\ x = X ) -> ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f <-> A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f ) )`
16 8 oveq1d
` |-  ( ( ph /\ x = X ) -> ( x H y ) = ( X H y ) )`
17 8 8 opeq12d
` |-  ( ( ph /\ x = X ) -> <. x , x >. = <. X , X >. )`
18 17 oveq1d
` |-  ( ( ph /\ x = X ) -> ( <. x , x >. .x. y ) = ( <. X , X >. .x. y ) )`
19 18 oveqd
` |-  ( ( ph /\ x = X ) -> ( f ( <. x , x >. .x. y ) g ) = ( f ( <. X , X >. .x. y ) g ) )`
20 19 eqeq1d
` |-  ( ( ph /\ x = X ) -> ( ( f ( <. x , x >. .x. y ) g ) = f <-> ( f ( <. X , X >. .x. y ) g ) = f ) )`
21 16 20 raleqbidv
` |-  ( ( ph /\ x = X ) -> ( A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f <-> A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) )`
22 15 21 anbi12d
` |-  ( ( ph /\ x = X ) -> ( ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) <-> ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) ) )`
23 22 ralbidv
` |-  ( ( ph /\ x = X ) -> ( A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) <-> A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) ) )`
24 9 23 riotaeqbidv
` |-  ( ( ph /\ x = X ) -> ( iota_ g e. ( x H x ) A. y e. B ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f /\ A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) ) = ( iota_ g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) ) )`
25 riotaex
` |-  ( iota_ g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) ) e. _V`
26 25 a1i
` |-  ( ph -> ( iota_ g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) ) e. _V )`
27 7 24 6 26 fvmptd
` |-  ( ph -> ( .1. ` X ) = ( iota_ g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) ) )`