Metamath Proof Explorer

Theorem termcfunc1eq

Description: Functors with terminal source are equal when they agree on its object. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypotheses termcfunc1eq.c 
|- ( ph -> C e. TermCat )
termcfunc1eq.f 
|- ( ph -> F e. ( C Func D ) )
termcfunc1eq.b 
|- B = ( Base ` C )
termcfunc1eq.g 
|- ( ph -> G e. ( C Func D ) )
termcfunc1eq.y 
|- ( ph -> Y e. B )
termcfunc1eq.e 
|- ( ph -> ( ( 1st ` F ) ` Y ) = ( ( 1st ` G ) ` Y ) )
Assertion termcfunc1eq 
|- ( ph -> F = G )

Proof

Step Hyp Ref Expression
1 termcfunc1eq.c 
 |-  ( ph -> C e. TermCat )
2 termcfunc1eq.f 
 |-  ( ph -> F e. ( C Func D ) )
3 termcfunc1eq.b 
 |-  B = ( Base ` C )
4 termcfunc1eq.g 
 |-  ( ph -> G e. ( C Func D ) )
5 termcfunc1eq.y 
 |-  ( ph -> Y e. B )
6 termcfunc1eq.e 
 |-  ( ph -> ( ( 1st ` F ) ` Y ) = ( ( 1st ` G ) ` Y ) )
7 6 opeq2d 
 |-  ( ph -> <. Y , ( ( 1st ` F ) ` Y ) >. = <. Y , ( ( 1st ` G ) ` Y ) >. )
8 7 sneqd 
 |-  ( ph -> { <. Y , ( ( 1st ` F ) ` Y ) >. } = { <. Y , ( ( 1st ` G ) ` Y ) >. } )
9 6 fveq2d 
 |-  ( ph -> ( ( Id ` D ) ` ( ( 1st ` F ) ` Y ) ) = ( ( Id ` D ) ` ( ( 1st ` G ) ` Y ) ) )
10 9 opeq2d 
 |-  ( ph -> <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` F ) ` Y ) ) >. = <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` G ) ` Y ) ) >. )
11 10 sneqd 
 |-  ( ph -> { <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` F ) ` Y ) ) >. } = { <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` G ) ` Y ) ) >. } )
12 11 opeq2d 
 |-  ( ph -> <. <. Y , Y >. , { <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` F ) ` Y ) ) >. } >. = <. <. Y , Y >. , { <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` G ) ` Y ) ) >. } >. )
13 12 sneqd 
 |-  ( ph -> { <. <. Y , Y >. , { <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` F ) ` Y ) ) >. } >. } = { <. <. Y , Y >. , { <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` G ) ` Y ) ) >. } >. } )
14 8 13 opeq12d 
 |-  ( ph -> <. { <. Y , ( ( 1st ` F ) ` Y ) >. } , { <. <. Y , Y >. , { <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` F ) ` Y ) ) >. } >. } >. = <. { <. Y , ( ( 1st ` G ) ` Y ) >. } , { <. <. Y , Y >. , { <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` G ) ` Y ) ) >. } >. } >. )
15 eqid 
 |-  ( Base ` D ) = ( Base ` D )
16 eqid 
 |-  ( ( 1st ` F ) ` Y ) = ( ( 1st ` F ) ` Y )
17 eqid 
 |-  ( Id ` D ) = ( Id ` D )
18 eqid 
 |-  ( Id ` C ) = ( Id ` C )
19 15 1 2 3 5 16 17 18 termcfuncval 
 |-  ( ph -> ( ( ( 1st ` F ) ` Y ) e. ( Base ` D ) /\ F = <. { <. Y , ( ( 1st ` F ) ` Y ) >. } , { <. <. Y , Y >. , { <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` F ) ` Y ) ) >. } >. } >. ) )
20 19 simprd 
 |-  ( ph -> F = <. { <. Y , ( ( 1st ` F ) ` Y ) >. } , { <. <. Y , Y >. , { <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` F ) ` Y ) ) >. } >. } >. )
21 eqid 
 |-  ( ( 1st ` G ) ` Y ) = ( ( 1st ` G ) ` Y )
22 15 1 4 3 5 21 17 18 termcfuncval 
 |-  ( ph -> ( ( ( 1st ` G ) ` Y ) e. ( Base ` D ) /\ G = <. { <. Y , ( ( 1st ` G ) ` Y ) >. } , { <. <. Y , Y >. , { <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` G ) ` Y ) ) >. } >. } >. ) )
23 22 simprd 
 |-  ( ph -> G = <. { <. Y , ( ( 1st ` G ) ` Y ) >. } , { <. <. Y , Y >. , { <. ( ( Id ` C ) ` Y ) , ( ( Id ` D ) ` ( ( 1st ` G ) ` Y ) ) >. } >. } >. )
24 14 20 23 3eqtr4d 
 |-  ( ph -> F = G )