Metamath Proof Explorer

Theorem termccofix

Description: Post-composition by an object-fixing endofunctor leaves a functor with terminal source literally unchanged. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypotheses termcfunc1eq.c 
|- ( ph -> C e. TermCat )
termcfunc1eq.f 
|- ( ph -> F e. ( C Func D ) )
termccofix.s 
|- ( ph -> S e. ( D Func D ) )
termccofix.i 
|- ( ph -> ( 1st ` S ) = ( _I |` A ) )
Assertion termccofix 
|- ( ph -> ( S o.func F ) = F )

Proof

Step Hyp Ref Expression
1 termcfunc1eq.c 
 |-  ( ph -> C e. TermCat )
2 termcfunc1eq.f 
 |-  ( ph -> F e. ( C Func D ) )
3 termccofix.s 
 |-  ( ph -> S e. ( D Func D ) )
4 termccofix.i 
 |-  ( ph -> ( 1st ` S ) = ( _I |` A ) )
5 2 3 cofucl 
 |-  ( ph -> ( S o.func F ) e. ( C Func D ) )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 1 6 termco 
 |-  ( ph -> U. ( Base ` C ) e. ( Base ` C ) )
8 6 2 3 7 cofu1 
 |-  ( ph -> ( ( 1st ` ( S o.func F ) ) ` U. ( Base ` C ) ) = ( ( 1st ` S ) ` ( ( 1st ` F ) ` U. ( Base ` C ) ) ) )
9 4 fveq1d 
 |-  ( ph -> ( ( 1st ` S ) ` ( ( 1st ` F ) ` U. ( Base ` C ) ) ) = ( ( _I |` A ) ` ( ( 1st ` F ) ` U. ( Base ` C ) ) ) )
10 eqid 
 |-  ( Base ` D ) = ( Base ` D )
11 2 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
12 6 10 11 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
13 12 7 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` F ) ` U. ( Base ` C ) ) e. ( Base ` D ) )
14 4 dmeqd 
 |-  ( ph -> dom ( 1st ` S ) = dom ( _I |` A ) )
15 dmresi 
 |-  dom ( _I |` A ) = A
16 14 15 eqtrdi 
 |-  ( ph -> dom ( 1st ` S ) = A )
17 3 func1st2nd 
 |-  ( ph -> ( 1st ` S ) ( D Func D ) ( 2nd ` S ) )
18 10 10 17 funcf1 
 |-  ( ph -> ( 1st ` S ) : ( Base ` D ) --> ( Base ` D ) )
19 18 fdmd 
 |-  ( ph -> dom ( 1st ` S ) = ( Base ` D ) )
20 16 19 eqtr3d 
 |-  ( ph -> A = ( Base ` D ) )
21 13 20 eleqtrrd 
 |-  ( ph -> ( ( 1st ` F ) ` U. ( Base ` C ) ) e. A )
22 fvresi 
 |-  ( ( ( 1st ` F ) ` U. ( Base ` C ) ) e. A -> ( ( _I |` A ) ` ( ( 1st ` F ) ` U. ( Base ` C ) ) ) = ( ( 1st ` F ) ` U. ( Base ` C ) ) )
23 21 22 syl 
 |-  ( ph -> ( ( _I |` A ) ` ( ( 1st ` F ) ` U. ( Base ` C ) ) ) = ( ( 1st ` F ) ` U. ( Base ` C ) ) )
24 8 9 23 3eqtrd 
 |-  ( ph -> ( ( 1st ` ( S o.func F ) ) ` U. ( Base ` C ) ) = ( ( 1st ` F ) ` U. ( Base ` C ) ) )
25 1 5 6 2 7 24 termcfunc1eq 
 |-  ( ph -> ( S o.func F ) = F )