Metamath Proof Explorer

Theorem catidd

Description: Deduce the identity arrow in a category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses catidd.b 
|- ( ph -> B = ( Base ` C ) )
catidd.h 
|- ( ph -> H = ( Hom ` C ) )
catidd.o 
|- ( ph -> .x. = ( comp ` C ) )
catidd.c 
|- ( ph -> C e. Cat )
catidd.1 
|- ( ( ph /\ x e. B ) -> .1. e. ( x H x ) )
catidd.2 
|- ( ( ph /\ ( x e. B /\ y e. B /\ f e. ( y H x ) ) ) -> ( .1. ( <. y , x >. .x. x ) f ) = f )
catidd.3 
|- ( ( ph /\ ( x e. B /\ y e. B /\ f e. ( x H y ) ) ) -> ( f ( <. x , x >. .x. y ) .1. ) = f )
Assertion catidd 
|- ( ph -> ( Id ` C ) = ( x e. B |-> .1. ) )

Proof

Step Hyp Ref Expression
1 catidd.b 
 |-  ( ph -> B = ( Base ` C ) )
2 catidd.h 
 |-  ( ph -> H = ( Hom ` C ) )
3 catidd.o 
 |-  ( ph -> .x. = ( comp ` C ) )
4 catidd.c 
 |-  ( ph -> C e. Cat )
5 catidd.1 
 |-  ( ( ph /\ x e. B ) -> .1. e. ( x H x ) )
6 catidd.2 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ f e. ( y H x ) ) ) -> ( .1. ( <. y , x >. .x. x ) f ) = f )
7 catidd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ f e. ( x H y ) ) ) -> ( f ( <. x , x >. .x. y ) .1. ) = f )
8 6 ex 
 |-  ( ph -> ( ( x e. B /\ y e. B /\ f e. ( y H x ) ) -> ( .1. ( <. y , x >. .x. x ) f ) = f ) )
9 1 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Base ` C ) ) )
10 1 eleq2d 
 |-  ( ph -> ( y e. B <-> y e. ( Base ` C ) ) )
11 2 oveqd 
 |-  ( ph -> ( y H x ) = ( y ( Hom ` C ) x ) )
12 11 eleq2d 
 |-  ( ph -> ( f e. ( y H x ) <-> f e. ( y ( Hom ` C ) x ) ) )
13 9 10 12 3anbi123d 
 |-  ( ph -> ( ( x e. B /\ y e. B /\ f e. ( y H x ) ) <-> ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( y ( Hom ` C ) x ) ) ) )
14 3 oveqd 
 |-  ( ph -> ( <. y , x >. .x. x ) = ( <. y , x >. ( comp ` C ) x ) )
15 14 oveqd 
 |-  ( ph -> ( .1. ( <. y , x >. .x. x ) f ) = ( .1. ( <. y , x >. ( comp ` C ) x ) f ) )
16 15 eqeq1d 
 |-  ( ph -> ( ( .1. ( <. y , x >. .x. x ) f ) = f <-> ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f ) )
17 8 13 16 3imtr3d 
 |-  ( ph -> ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f ) )
18 17 3expd 
 |-  ( ph -> ( x e. ( Base ` C ) -> ( y e. ( Base ` C ) -> ( f e. ( y ( Hom ` C ) x ) -> ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f ) ) ) )
19 18 imp41 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f )
20 19 ralrimiva 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) -> A. f e. ( y ( Hom ` C ) x ) ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f )
21 7 ex 
 |-  ( ph -> ( ( x e. B /\ y e. B /\ f e. ( x H y ) ) -> ( f ( <. x , x >. .x. y ) .1. ) = f ) )
22 2 oveqd 
 |-  ( ph -> ( x H y ) = ( x ( Hom ` C ) y ) )
23 22 eleq2d 
 |-  ( ph -> ( f e. ( x H y ) <-> f e. ( x ( Hom ` C ) y ) ) )
24 9 10 23 3anbi123d 
 |-  ( ph -> ( ( x e. B /\ y e. B /\ f e. ( x H y ) ) <-> ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) ) )
25 3 oveqd 
 |-  ( ph -> ( <. x , x >. .x. y ) = ( <. x , x >. ( comp ` C ) y ) )
26 25 oveqd 
 |-  ( ph -> ( f ( <. x , x >. .x. y ) .1. ) = ( f ( <. x , x >. ( comp ` C ) y ) .1. ) )
27 26 eqeq1d 
 |-  ( ph -> ( ( f ( <. x , x >. .x. y ) .1. ) = f <-> ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f ) )
28 21 24 27 3imtr3d 
 |-  ( ph -> ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f ) )
29 28 3expd 
 |-  ( ph -> ( x e. ( Base ` C ) -> ( y e. ( Base ` C ) -> ( f e. ( x ( Hom ` C ) y ) -> ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f ) ) ) )
30 29 imp41 
 |-  ( ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f )
31 30 ralrimiva 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) -> A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f )
32 20 31 jca 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ y e. ( Base ` C ) ) -> ( A. f e. ( y ( Hom ` C ) x ) ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f ) )
33 32 ralrimiva 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f ) )
34 5 ex 
 |-  ( ph -> ( x e. B -> .1. e. ( x H x ) ) )
35 2 oveqd 
 |-  ( ph -> ( x H x ) = ( x ( Hom ` C ) x ) )
36 35 eleq2d 
 |-  ( ph -> ( .1. e. ( x H x ) <-> .1. e. ( x ( Hom ` C ) x ) ) )
37 34 9 36 3imtr3d 
 |-  ( ph -> ( x e. ( Base ` C ) -> .1. e. ( x ( Hom ` C ) x ) ) )
38 37 imp 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> .1. e. ( x ( Hom ` C ) x ) )
39 eqid 
 |-  ( Base ` C ) = ( Base ` C )
40 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
41 eqid 
 |-  ( comp ` C ) = ( comp ` C )
42 4 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> C e. Cat )
43 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
44 39 40 41 42 43 catideu 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> E! g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) )
45 oveq1 
 |-  ( g = .1. -> ( g ( <. y , x >. ( comp ` C ) x ) f ) = ( .1. ( <. y , x >. ( comp ` C ) x ) f ) )
46 45 eqeq1d 
 |-  ( g = .1. -> ( ( g ( <. y , x >. ( comp ` C ) x ) f ) = f <-> ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f ) )
47 46 ralbidv 
 |-  ( g = .1. -> ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f <-> A. f e. ( y ( Hom ` C ) x ) ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f ) )
48 oveq2 
 |-  ( g = .1. -> ( f ( <. x , x >. ( comp ` C ) y ) g ) = ( f ( <. x , x >. ( comp ` C ) y ) .1. ) )
49 48 eqeq1d 
 |-  ( g = .1. -> ( ( f ( <. x , x >. ( comp ` C ) y ) g ) = f <-> ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f ) )
50 49 ralbidv 
 |-  ( g = .1. -> ( A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f <-> A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f ) )
51 47 50 anbi12d 
 |-  ( g = .1. -> ( ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) <-> ( A. f e. ( y ( Hom ` C ) x ) ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f ) ) )
52 51 ralbidv 
 |-  ( g = .1. -> ( A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) <-> A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f ) ) )
53 52 riota2 
 |-  ( ( .1. e. ( x ( Hom ` C ) x ) /\ E! g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) -> ( A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f ) <-> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) = .1. ) )
54 38 44 53 syl2anc 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( .1. ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) .1. ) = f ) <-> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) = .1. ) )
55 33 54 mpbid 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) = .1. )
56 55 mpteq2dva 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) ) = ( x e. ( Base ` C ) |-> .1. ) )
57 eqid 
 |-  ( Id ` C ) = ( Id ` C )
58 39 40 41 4 57 cidfval 
 |-  ( ph -> ( Id ` C ) = ( x e. ( Base ` C ) |-> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) ) )
59 1 mpteq1d 
 |-  ( ph -> ( x e. B |-> .1. ) = ( x e. ( Base ` C ) |-> .1. ) )
60 56 58 59 3eqtr4d 
 |-  ( ph -> ( Id ` C ) = ( x e. B |-> .1. ) )