Metamath Proof Explorer

Theorem fucoid

Description: Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid2 . (Contributed by Zhi Wang, 30-Sep-2025)

Ref Expression
Hypotheses fucoid.o 
|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
fucoid.t 
|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
fucoid.1 
|- .1. = ( Id ` T )
fucoid.q 
|- Q = ( C FuncCat E )
fucoid.i 
|- I = ( Id ` Q )
fucoid.f 
|- ( ph -> F ( C Func D ) G )
fucoid.k 
|- ( ph -> K ( D Func E ) L )
fucoid.u 
|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
Assertion fucoid 
|- ( ph -> ( ( U P U ) ` ( .1. ` U ) ) = ( I ` ( O ` U ) ) )

Proof

Step Hyp Ref Expression
1 fucoid.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2 fucoid.t 
 |-  T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
3 fucoid.1 
 |-  .1. = ( Id ` T )
4 fucoid.q 
 |-  Q = ( C FuncCat E )
5 fucoid.i 
 |-  I = ( Id ` Q )
6 fucoid.f 
 |-  ( ph -> F ( C Func D ) G )
7 fucoid.k 
 |-  ( ph -> K ( D Func E ) L )
8 fucoid.u 
 |-  ( ph -> U = <. <. K , L >. , <. F , G >. >. )
9 ovex 
 |-  ( ( ( ( Id ` E ) o. K ) ` ( F ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. ( comp ` E ) ( K ` ( F ` x ) ) ) ( ( ( F ` x ) L ( F ` x ) ) ` ( ( ( Id ` D ) o. F ) ` x ) ) ) e. _V
10 eqid 
 |-  ( x e. ( Base ` C ) |-> ( ( ( ( Id ` E ) o. K ) ` ( F ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. ( comp ` E ) ( K ` ( F ` x ) ) ) ( ( ( F ` x ) L ( F ` x ) ) ` ( ( ( Id ` D ) o. F ) ` x ) ) ) ) = ( x e. ( Base ` C ) |-> ( ( ( ( Id ` E ) o. K ) ` ( F ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. ( comp ` E ) ( K ` ( F ` x ) ) ) ( ( ( F ` x ) L ( F ` x ) ) ` ( ( ( Id ` D ) o. F ) ` x ) ) ) )
11 9 10 fnmpti 
 |-  ( x e. ( Base ` C ) |-> ( ( ( ( Id ` E ) o. K ) ` ( F ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. ( comp ` E ) ( K ` ( F ` x ) ) ) ( ( ( F ` x ) L ( F ` x ) ) ` ( ( ( Id ` D ) o. F ) ` x ) ) ) ) Fn ( Base ` C )
12 11 a1i 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( ( ( Id ` E ) o. K ) ` ( F ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. ( comp ` E ) ( K ` ( F ` x ) ) ) ( ( ( F ` x ) L ( F ` x ) ) ` ( ( ( Id ` D ) o. F ) ` x ) ) ) ) Fn ( Base ` C ) )
13 7 funcrcl3 
 |-  ( ph -> E e. Cat )
14 eqid 
 |-  ( Base ` E ) = ( Base ` E )
15 eqid 
 |-  ( Id ` E ) = ( Id ` E )
16 14 15 cidfn 
 |-  ( E e. Cat -> ( Id ` E ) Fn ( Base ` E ) )
17 13 16 syl 
 |-  ( ph -> ( Id ` E ) Fn ( Base ` E ) )
18 eqid 
 |-  ( Base ` D ) = ( Base ` D )
19 18 14 7 funcf1 
 |-  ( ph -> K : ( Base ` D ) --> ( Base ` E ) )
20 eqid 
 |-  ( Base ` C ) = ( Base ` C )
21 20 18 6 funcf1 
 |-  ( ph -> F : ( Base ` C ) --> ( Base ` D ) )
22 19 21 fcod 
 |-  ( ph -> ( K o. F ) : ( Base ` C ) --> ( Base ` E ) )
23 fnfco 
 |-  ( ( ( Id ` E ) Fn ( Base ` E ) /\ ( K o. F ) : ( Base ` C ) --> ( Base ` E ) ) -> ( ( Id ` E ) o. ( K o. F ) ) Fn ( Base ` C ) )
24 17 22 23 syl2anc 
 |-  ( ph -> ( ( Id ` E ) o. ( K o. F ) ) Fn ( Base ` C ) )
25 2fveq3 
 |-  ( x = w -> ( K ` ( F ` x ) ) = ( K ` ( F ` w ) ) )
26 25 25 opeq12d 
 |-  ( x = w -> <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. = <. ( K ` ( F ` w ) ) , ( K ` ( F ` w ) ) >. )
27 26 25 oveq12d 
 |-  ( x = w -> ( <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. ( comp ` E ) ( K ` ( F ` x ) ) ) = ( <. ( K ` ( F ` w ) ) , ( K ` ( F ` w ) ) >. ( comp ` E ) ( K ` ( F ` w ) ) ) )
28 2fveq3 
 |-  ( x = w -> ( ( ( Id ` E ) o. K ) ` ( F ` x ) ) = ( ( ( Id ` E ) o. K ) ` ( F ` w ) ) )
29 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
30 29 29 oveq12d 
 |-  ( x = w -> ( ( F ` x ) L ( F ` x ) ) = ( ( F ` w ) L ( F ` w ) ) )
31 fveq2 
 |-  ( x = w -> ( ( ( Id ` D ) o. F ) ` x ) = ( ( ( Id ` D ) o. F ) ` w ) )
32 30 31 fveq12d 
 |-  ( x = w -> ( ( ( F ` x ) L ( F ` x ) ) ` ( ( ( Id ` D ) o. F ) ` x ) ) = ( ( ( F ` w ) L ( F ` w ) ) ` ( ( ( Id ` D ) o. F ) ` w ) ) )
33 27 28 32 oveq123d 
 |-  ( x = w -> ( ( ( ( Id ` E ) o. K ) ` ( F ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. ( comp ` E ) ( K ` ( F ` x ) ) ) ( ( ( F ` x ) L ( F ` x ) ) ` ( ( ( Id ` D ) o. F ) ` x ) ) ) = ( ( ( ( Id ` E ) o. K ) ` ( F ` w ) ) ( <. ( K ` ( F ` w ) ) , ( K ` ( F ` w ) ) >. ( comp ` E ) ( K ` ( F ` w ) ) ) ( ( ( F ` w ) L ( F ` w ) ) ` ( ( ( Id ` D ) o. F ) ` w ) ) ) )
34 simpr 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> w e. ( Base ` C ) )
35 ovexd 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( ( ( Id ` E ) o. K ) ` ( F ` w ) ) ( <. ( K ` ( F ` w ) ) , ( K ` ( F ` w ) ) >. ( comp ` E ) ( K ` ( F ` w ) ) ) ( ( ( F ` w ) L ( F ` w ) ) ` ( ( ( Id ` D ) o. F ) ` w ) ) ) e. _V )
36 10 33 34 35 fvmptd3 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( x e. ( Base ` C ) |-> ( ( ( ( Id ` E ) o. K ) ` ( F ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. ( comp ` E ) ( K ` ( F ` x ) ) ) ( ( ( F ` x ) L ( F ` x ) ) ` ( ( ( Id ` D ) o. F ) ` x ) ) ) ) ` w ) = ( ( ( ( Id ` E ) o. K ) ` ( F ` w ) ) ( <. ( K ` ( F ` w ) ) , ( K ` ( F ` w ) ) >. ( comp ` E ) ( K ` ( F ` w ) ) ) ( ( ( F ` w ) L ( F ` w ) ) ` ( ( ( Id ` D ) o. F ) ` w ) ) ) )
37 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
38 13 adantr 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> E e. Cat )
39 19 adantr 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> K : ( Base ` D ) --> ( Base ` E ) )
40 21 ffvelcdmda 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( F ` w ) e. ( Base ` D ) )
41 39 40 ffvelcdmd 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( K ` ( F ` w ) ) e. ( Base ` E ) )
42 eqid 
 |-  ( comp ` E ) = ( comp ` E )
43 14 37 15 38 41 catidcl 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( Id ` E ) ` ( K ` ( F ` w ) ) ) e. ( ( K ` ( F ` w ) ) ( Hom ` E ) ( K ` ( F ` w ) ) ) )
44 14 37 15 38 41 42 41 43 catlid 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( ( Id ` E ) ` ( K ` ( F ` w ) ) ) ( <. ( K ` ( F ` w ) ) , ( K ` ( F ` w ) ) >. ( comp ` E ) ( K ` ( F ` w ) ) ) ( ( Id ` E ) ` ( K ` ( F ` w ) ) ) ) = ( ( Id ` E ) ` ( K ` ( F ` w ) ) ) )
45 39 40 fvco3d 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( ( Id ` E ) o. K ) ` ( F ` w ) ) = ( ( Id ` E ) ` ( K ` ( F ` w ) ) ) )
46 21 adantr 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> F : ( Base ` C ) --> ( Base ` D ) )
47 46 34 fvco3d 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( ( Id ` D ) o. F ) ` w ) = ( ( Id ` D ) ` ( F ` w ) ) )
48 47 fveq2d 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( ( F ` w ) L ( F ` w ) ) ` ( ( ( Id ` D ) o. F ) ` w ) ) = ( ( ( F ` w ) L ( F ` w ) ) ` ( ( Id ` D ) ` ( F ` w ) ) ) )
49 eqid 
 |-  ( Id ` D ) = ( Id ` D )
50 7 adantr 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> K ( D Func E ) L )
51 18 49 15 50 40 funcid 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( ( F ` w ) L ( F ` w ) ) ` ( ( Id ` D ) ` ( F ` w ) ) ) = ( ( Id ` E ) ` ( K ` ( F ` w ) ) ) )
52 48 51 eqtrd 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( ( F ` w ) L ( F ` w ) ) ` ( ( ( Id ` D ) o. F ) ` w ) ) = ( ( Id ` E ) ` ( K ` ( F ` w ) ) ) )
53 45 52 oveq12d 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( ( ( Id ` E ) o. K ) ` ( F ` w ) ) ( <. ( K ` ( F ` w ) ) , ( K ` ( F ` w ) ) >. ( comp ` E ) ( K ` ( F ` w ) ) ) ( ( ( F ` w ) L ( F ` w ) ) ` ( ( ( Id ` D ) o. F ) ` w ) ) ) = ( ( ( Id ` E ) ` ( K ` ( F ` w ) ) ) ( <. ( K ` ( F ` w ) ) , ( K ` ( F ` w ) ) >. ( comp ` E ) ( K ` ( F ` w ) ) ) ( ( Id ` E ) ` ( K ` ( F ` w ) ) ) ) )
54 22 adantr 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( K o. F ) : ( Base ` C ) --> ( Base ` E ) )
55 54 34 fvco3d 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( ( Id ` E ) o. ( K o. F ) ) ` w ) = ( ( Id ` E ) ` ( ( K o. F ) ` w ) ) )
56 46 34 fvco3d 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( K o. F ) ` w ) = ( K ` ( F ` w ) ) )
57 56 fveq2d 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( Id ` E ) ` ( ( K o. F ) ` w ) ) = ( ( Id ` E ) ` ( K ` ( F ` w ) ) ) )
58 55 57 eqtrd 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( ( Id ` E ) o. ( K o. F ) ) ` w ) = ( ( Id ` E ) ` ( K ` ( F ` w ) ) ) )
59 44 53 58 3eqtr4d 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( ( ( Id ` E ) o. K ) ` ( F ` w ) ) ( <. ( K ` ( F ` w ) ) , ( K ` ( F ` w ) ) >. ( comp ` E ) ( K ` ( F ` w ) ) ) ( ( ( F ` w ) L ( F ` w ) ) ` ( ( ( Id ` D ) o. F ) ` w ) ) ) = ( ( ( Id ` E ) o. ( K o. F ) ) ` w ) )
60 36 59 eqtrd 
 |-  ( ( ph /\ w e. ( Base ` C ) ) -> ( ( x e. ( Base ` C ) |-> ( ( ( ( Id ` E ) o. K ) ` ( F ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. ( comp ` E ) ( K ` ( F ` x ) ) ) ( ( ( F ` x ) L ( F ` x ) ) ` ( ( ( Id ` D ) o. F ) ` x ) ) ) ) ` w ) = ( ( ( Id ` E ) o. ( K o. F ) ) ` w ) )
61 12 24 60 eqfnfvd 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( ( ( Id ` E ) o. K ) ` ( F ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. ( comp ` E ) ( K ` ( F ` x ) ) ) ( ( ( F ` x ) L ( F ` x ) ) ` ( ( ( Id ` D ) o. F ) ` x ) ) ) ) = ( ( Id ` E ) o. ( K o. F ) ) )
62 8 fveq2d 
 |-  ( ph -> ( .1. ` U ) = ( .1. ` <. <. K , L >. , <. F , G >. >. ) )
63 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
64 7 funcrcl2 
 |-  ( ph -> D e. Cat )
65 63 64 13 fuccat 
 |-  ( ph -> ( D FuncCat E ) e. Cat )
66 eqid 
 |-  ( C FuncCat D ) = ( C FuncCat D )
67 6 funcrcl2 
 |-  ( ph -> C e. Cat )
68 66 67 64 fuccat 
 |-  ( ph -> ( C FuncCat D ) e. Cat )
69 63 fucbas 
 |-  ( D Func E ) = ( Base ` ( D FuncCat E ) )
70 66 fucbas 
 |-  ( C Func D ) = ( Base ` ( C FuncCat D ) )
71 eqid 
 |-  ( Id ` ( D FuncCat E ) ) = ( Id ` ( D FuncCat E ) )
72 eqid 
 |-  ( Id ` ( C FuncCat D ) ) = ( Id ` ( C FuncCat D ) )
73 df-br 
 |-  ( K ( D Func E ) L <-> <. K , L >. e. ( D Func E ) )
74 7 73 sylib 
 |-  ( ph -> <. K , L >. e. ( D Func E ) )
75 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
76 6 75 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
77 2 65 68 69 70 71 72 3 74 76 xpcid 
 |-  ( ph -> ( .1. ` <. <. K , L >. , <. F , G >. >. ) = <. ( ( Id ` ( D FuncCat E ) ) ` <. K , L >. ) , ( ( Id ` ( C FuncCat D ) ) ` <. F , G >. ) >. )
78 63 71 15 74 fucid 
 |-  ( ph -> ( ( Id ` ( D FuncCat E ) ) ` <. K , L >. ) = ( ( Id ` E ) o. ( 1st ` <. K , L >. ) ) )
79 relfunc 
 |-  Rel ( D Func E )
80 79 brrelex1i 
 |-  ( K ( D Func E ) L -> K e. _V )
81 7 80 syl 
 |-  ( ph -> K e. _V )
82 79 brrelex2i 
 |-  ( K ( D Func E ) L -> L e. _V )
83 7 82 syl 
 |-  ( ph -> L e. _V )
84 op1stg 
 |-  ( ( K e. _V /\ L e. _V ) -> ( 1st ` <. K , L >. ) = K )
85 81 83 84 syl2anc 
 |-  ( ph -> ( 1st ` <. K , L >. ) = K )
86 85 coeq2d 
 |-  ( ph -> ( ( Id ` E ) o. ( 1st ` <. K , L >. ) ) = ( ( Id ` E ) o. K ) )
87 78 86 eqtrd 
 |-  ( ph -> ( ( Id ` ( D FuncCat E ) ) ` <. K , L >. ) = ( ( Id ` E ) o. K ) )
88 66 72 49 76 fucid 
 |-  ( ph -> ( ( Id ` ( C FuncCat D ) ) ` <. F , G >. ) = ( ( Id ` D ) o. ( 1st ` <. F , G >. ) ) )
89 relfunc 
 |-  Rel ( C Func D )
90 89 brrelex1i 
 |-  ( F ( C Func D ) G -> F e. _V )
91 6 90 syl 
 |-  ( ph -> F e. _V )
92 89 brrelex2i 
 |-  ( F ( C Func D ) G -> G e. _V )
93 6 92 syl 
 |-  ( ph -> G e. _V )
94 op1stg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 1st ` <. F , G >. ) = F )
95 91 93 94 syl2anc 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
96 95 coeq2d 
 |-  ( ph -> ( ( Id ` D ) o. ( 1st ` <. F , G >. ) ) = ( ( Id ` D ) o. F ) )
97 88 96 eqtrd 
 |-  ( ph -> ( ( Id ` ( C FuncCat D ) ) ` <. F , G >. ) = ( ( Id ` D ) o. F ) )
98 87 97 opeq12d 
 |-  ( ph -> <. ( ( Id ` ( D FuncCat E ) ) ` <. K , L >. ) , ( ( Id ` ( C FuncCat D ) ) ` <. F , G >. ) >. = <. ( ( Id ` E ) o. K ) , ( ( Id ` D ) o. F ) >. )
99 62 77 98 3eqtrd 
 |-  ( ph -> ( .1. ` U ) = <. ( ( Id ` E ) o. K ) , ( ( Id ` D ) o. F ) >. )
100 99 fveq2d 
 |-  ( ph -> ( ( U P U ) ` ( .1. ` U ) ) = ( ( U P U ) ` <. ( ( Id ` E ) o. K ) , ( ( Id ` D ) o. F ) >. ) )
101 df-ov 
 |-  ( ( ( Id ` E ) o. K ) ( U P U ) ( ( Id ` D ) o. F ) ) = ( ( U P U ) ` <. ( ( Id ` E ) o. K ) , ( ( Id ` D ) o. F ) >. )
102 100 101 eqtr4di 
 |-  ( ph -> ( ( U P U ) ` ( .1. ` U ) ) = ( ( ( Id ` E ) o. K ) ( U P U ) ( ( Id ` D ) o. F ) ) )
103 eqid 
 |-  ( C Nat D ) = ( C Nat D )
104 66 103 fuchom 
 |-  ( C Nat D ) = ( Hom ` ( C FuncCat D ) )
105 70 104 72 68 76 catidcl 
 |-  ( ph -> ( ( Id ` ( C FuncCat D ) ) ` <. F , G >. ) e. ( <. F , G >. ( C Nat D ) <. F , G >. ) )
106 97 105 eqeltrrd 
 |-  ( ph -> ( ( Id ` D ) o. F ) e. ( <. F , G >. ( C Nat D ) <. F , G >. ) )
107 eqid 
 |-  ( D Nat E ) = ( D Nat E )
108 63 107 fuchom 
 |-  ( D Nat E ) = ( Hom ` ( D FuncCat E ) )
109 69 108 71 65 74 catidcl 
 |-  ( ph -> ( ( Id ` ( D FuncCat E ) ) ` <. K , L >. ) e. ( <. K , L >. ( D Nat E ) <. K , L >. ) )
110 87 109 eqeltrrd 
 |-  ( ph -> ( ( Id ` E ) o. K ) e. ( <. K , L >. ( D Nat E ) <. K , L >. ) )
111 1 8 8 106 110 fuco22 
 |-  ( ph -> ( ( ( Id ` E ) o. K ) ( U P U ) ( ( Id ` D ) o. F ) ) = ( x e. ( Base ` C ) |-> ( ( ( ( Id ` E ) o. K ) ` ( F ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. ( comp ` E ) ( K ` ( F ` x ) ) ) ( ( ( F ` x ) L ( F ` x ) ) ` ( ( ( Id ` D ) o. F ) ` x ) ) ) ) )
112 102 111 eqtrd 
 |-  ( ph -> ( ( U P U ) ` ( .1. ` U ) ) = ( x e. ( Base ` C ) |-> ( ( ( ( Id ` E ) o. K ) ` ( F ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( F ` x ) ) >. ( comp ` E ) ( K ` ( F ` x ) ) ) ( ( ( F ` x ) L ( F ` x ) ) ` ( ( ( Id ` D ) o. F ) ` x ) ) ) ) )
113 1 6 7 8 4 5 15 fuco11id 
 |-  ( ph -> ( I ` ( O ` U ) ) = ( ( Id ` E ) o. ( K o. F ) ) )
114 61 112 113 3eqtr4d 
 |-  ( ph -> ( ( U P U ) ` ( .1. ` U ) ) = ( I ` ( O ` U ) ) )