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. ) ) |