Metamath Proof Explorer

Theorem termcfuncval

Description: The value of a functor from a terminal category. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypotheses diag1f1o.a 
|- A = ( Base ` C )
diag1f1o.d 
|- ( ph -> D e. TermCat )
termcfuncval.k 
|- ( ph -> K e. ( D Func C ) )
termcfuncval.b 
|- B = ( Base ` D )
termcfuncval.y 
|- ( ph -> Y e. B )
termcfuncval.x 
|- X = ( ( 1st ` K ) ` Y )
termcfuncval.1 
|- .1. = ( Id ` C )
termcfuncval.i 
|- I = ( Id ` D )
Assertion termcfuncval 
|- ( ph -> ( X e. A /\ K = <. { <. Y , X >. } , { <. <. Y , Y >. , { <. ( I ` Y ) , ( .1. ` X ) >. } >. } >. ) )

Proof

Step Hyp Ref Expression
1 diag1f1o.a 
 |-  A = ( Base ` C )
2 diag1f1o.d 
 |-  ( ph -> D e. TermCat )
3 termcfuncval.k 
 |-  ( ph -> K e. ( D Func C ) )
4 termcfuncval.b 
 |-  B = ( Base ` D )
5 termcfuncval.y 
 |-  ( ph -> Y e. B )
6 termcfuncval.x 
 |-  X = ( ( 1st ` K ) ` Y )
7 termcfuncval.1 
 |-  .1. = ( Id ` C )
8 termcfuncval.i 
 |-  I = ( Id ` D )
9 3 func1st2nd 
 |-  ( ph -> ( 1st ` K ) ( D Func C ) ( 2nd ` K ) )
10 4 1 9 funcf1 
 |-  ( ph -> ( 1st ` K ) : B --> A )
11 10 5 ffvelcdmd 
 |-  ( ph -> ( ( 1st ` K ) ` Y ) e. A )
12 6 11 eqeltrid 
 |-  ( ph -> X e. A )
13 relfunc 
 |-  Rel ( D Func C )
14 1st2nd 
 |-  ( ( Rel ( D Func C ) /\ K e. ( D Func C ) ) -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
15 13 3 14 sylancr 
 |-  ( ph -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
16 2 4 5 termcbas2 
 |-  ( ph -> B = { Y } )
17 16 feq2d 
 |-  ( ph -> ( ( 1st ` K ) : B --> A <-> ( 1st ` K ) : { Y } --> A ) )
18 10 17 mpbid 
 |-  ( ph -> ( 1st ` K ) : { Y } --> A )
19 fsn2g 
 |-  ( Y e. B -> ( ( 1st ` K ) : { Y } --> A <-> ( ( ( 1st ` K ) ` Y ) e. A /\ ( 1st ` K ) = { <. Y , ( ( 1st ` K ) ` Y ) >. } ) ) )
20 5 19 syl 
 |-  ( ph -> ( ( 1st ` K ) : { Y } --> A <-> ( ( ( 1st ` K ) ` Y ) e. A /\ ( 1st ` K ) = { <. Y , ( ( 1st ` K ) ` Y ) >. } ) ) )
21 18 20 mpbid 
 |-  ( ph -> ( ( ( 1st ` K ) ` Y ) e. A /\ ( 1st ` K ) = { <. Y , ( ( 1st ` K ) ` Y ) >. } ) )
22 21 simprd 
 |-  ( ph -> ( 1st ` K ) = { <. Y , ( ( 1st ` K ) ` Y ) >. } )
23 6 opeq2i 
 |-  <. Y , X >. = <. Y , ( ( 1st ` K ) ` Y ) >.
24 23 sneqi 
 |-  { <. Y , X >. } = { <. Y , ( ( 1st ` K ) ` Y ) >. }
25 22 24 eqtr4di 
 |-  ( ph -> ( 1st ` K ) = { <. Y , X >. } )
26 4 9 funcfn2 
 |-  ( ph -> ( 2nd ` K ) Fn ( B X. B ) )
27 16 sqxpeqd 
 |-  ( ph -> ( B X. B ) = ( { Y } X. { Y } ) )
28 xpsng 
 |-  ( ( Y e. B /\ Y e. B ) -> ( { Y } X. { Y } ) = { <. Y , Y >. } )
29 5 5 28 syl2anc 
 |-  ( ph -> ( { Y } X. { Y } ) = { <. Y , Y >. } )
30 27 29 eqtrd 
 |-  ( ph -> ( B X. B ) = { <. Y , Y >. } )
31 30 fneq2d 
 |-  ( ph -> ( ( 2nd ` K ) Fn ( B X. B ) <-> ( 2nd ` K ) Fn { <. Y , Y >. } ) )
32 26 31 mpbid 
 |-  ( ph -> ( 2nd ` K ) Fn { <. Y , Y >. } )
33 opex 
 |-  <. Y , Y >. e. _V
34 33 fnsnb 
 |-  ( ( 2nd ` K ) Fn { <. Y , Y >. } <-> ( 2nd ` K ) = { <. <. Y , Y >. , ( ( 2nd ` K ) ` <. Y , Y >. ) >. } )
35 32 34 sylib 
 |-  ( ph -> ( 2nd ` K ) = { <. <. Y , Y >. , ( ( 2nd ` K ) ` <. Y , Y >. ) >. } )
36 df-ov 
 |-  ( Y ( 2nd ` K ) Y ) = ( ( 2nd ` K ) ` <. Y , Y >. )
37 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
38 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
39 4 37 38 9 5 5 funcf2 
 |-  ( ph -> ( Y ( 2nd ` K ) Y ) : ( Y ( Hom ` D ) Y ) --> ( ( ( 1st ` K ) ` Y ) ( Hom ` C ) ( ( 1st ` K ) ` Y ) ) )
40 2 4 5 5 37 8 termchom 
 |-  ( ph -> ( Y ( Hom ` D ) Y ) = { ( I ` Y ) } )
41 40 eqcomd 
 |-  ( ph -> { ( I ` Y ) } = ( Y ( Hom ` D ) Y ) )
42 6 6 oveq12i 
 |-  ( X ( Hom ` C ) X ) = ( ( ( 1st ` K ) ` Y ) ( Hom ` C ) ( ( 1st ` K ) ` Y ) )
43 42 a1i 
 |-  ( ph -> ( X ( Hom ` C ) X ) = ( ( ( 1st ` K ) ` Y ) ( Hom ` C ) ( ( 1st ` K ) ` Y ) ) )
44 41 43 feq23d 
 |-  ( ph -> ( ( Y ( 2nd ` K ) Y ) : { ( I ` Y ) } --> ( X ( Hom ` C ) X ) <-> ( Y ( 2nd ` K ) Y ) : ( Y ( Hom ` D ) Y ) --> ( ( ( 1st ` K ) ` Y ) ( Hom ` C ) ( ( 1st ` K ) ` Y ) ) ) )
45 39 44 mpbird 
 |-  ( ph -> ( Y ( 2nd ` K ) Y ) : { ( I ` Y ) } --> ( X ( Hom ` C ) X ) )
46 fvex 
 |-  ( I ` Y ) e. _V
47 46 fsn2 
 |-  ( ( Y ( 2nd ` K ) Y ) : { ( I ` Y ) } --> ( X ( Hom ` C ) X ) <-> ( ( ( Y ( 2nd ` K ) Y ) ` ( I ` Y ) ) e. ( X ( Hom ` C ) X ) /\ ( Y ( 2nd ` K ) Y ) = { <. ( I ` Y ) , ( ( Y ( 2nd ` K ) Y ) ` ( I ` Y ) ) >. } ) )
48 45 47 sylib 
 |-  ( ph -> ( ( ( Y ( 2nd ` K ) Y ) ` ( I ` Y ) ) e. ( X ( Hom ` C ) X ) /\ ( Y ( 2nd ` K ) Y ) = { <. ( I ` Y ) , ( ( Y ( 2nd ` K ) Y ) ` ( I ` Y ) ) >. } ) )
49 48 simprd 
 |-  ( ph -> ( Y ( 2nd ` K ) Y ) = { <. ( I ` Y ) , ( ( Y ( 2nd ` K ) Y ) ` ( I ` Y ) ) >. } )
50 4 8 7 9 5 funcid 
 |-  ( ph -> ( ( Y ( 2nd ` K ) Y ) ` ( I ` Y ) ) = ( .1. ` ( ( 1st ` K ) ` Y ) ) )
51 6 fveq2i 
 |-  ( .1. ` X ) = ( .1. ` ( ( 1st ` K ) ` Y ) )
52 50 51 eqtr4di 
 |-  ( ph -> ( ( Y ( 2nd ` K ) Y ) ` ( I ` Y ) ) = ( .1. ` X ) )
53 52 opeq2d 
 |-  ( ph -> <. ( I ` Y ) , ( ( Y ( 2nd ` K ) Y ) ` ( I ` Y ) ) >. = <. ( I ` Y ) , ( .1. ` X ) >. )
54 53 sneqd 
 |-  ( ph -> { <. ( I ` Y ) , ( ( Y ( 2nd ` K ) Y ) ` ( I ` Y ) ) >. } = { <. ( I ` Y ) , ( .1. ` X ) >. } )
55 49 54 eqtrd 
 |-  ( ph -> ( Y ( 2nd ` K ) Y ) = { <. ( I ` Y ) , ( .1. ` X ) >. } )
56 36 55 eqtr3id 
 |-  ( ph -> ( ( 2nd ` K ) ` <. Y , Y >. ) = { <. ( I ` Y ) , ( .1. ` X ) >. } )
57 56 opeq2d 
 |-  ( ph -> <. <. Y , Y >. , ( ( 2nd ` K ) ` <. Y , Y >. ) >. = <. <. Y , Y >. , { <. ( I ` Y ) , ( .1. ` X ) >. } >. )
58 57 sneqd 
 |-  ( ph -> { <. <. Y , Y >. , ( ( 2nd ` K ) ` <. Y , Y >. ) >. } = { <. <. Y , Y >. , { <. ( I ` Y ) , ( .1. ` X ) >. } >. } )
59 35 58 eqtrd 
 |-  ( ph -> ( 2nd ` K ) = { <. <. Y , Y >. , { <. ( I ` Y ) , ( .1. ` X ) >. } >. } )
60 25 59 opeq12d 
 |-  ( ph -> <. ( 1st ` K ) , ( 2nd ` K ) >. = <. { <. Y , X >. } , { <. <. Y , Y >. , { <. ( I ` Y ) , ( .1. ` X ) >. } >. } >. )
61 15 60 eqtrd 
 |-  ( ph -> K = <. { <. Y , X >. } , { <. <. Y , Y >. , { <. ( I ` Y ) , ( .1. ` X ) >. } >. } >. )
62 12 61 jca 
 |-  ( ph -> ( X e. A /\ K = <. { <. Y , X >. } , { <. <. Y , Y >. , { <. ( I ` Y ) , ( .1. ` X ) >. } >. } >. ) )