Metamath Proof Explorer

Theorem diag1f1olem

Description: To any functor from a terminal category can an object in the target base be assigned. (Contributed by Zhi Wang, 21-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 )
diag1f1olem.l 
|- L = ( C DiagFunc D )
Assertion diag1f1olem 
|- ( ph -> ( X e. A /\ K = ( ( 1st ` L ) ` 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 diag1f1olem.l 
 |-  L = ( C DiagFunc D )
8 eqid 
 |-  ( Id ` C ) = ( Id ` C )
9 eqid 
 |-  ( Id ` D ) = ( Id ` D )
10 1 2 3 4 5 6 8 9 termcfuncval 
 |-  ( ph -> ( X e. A /\ K = <. { <. Y , X >. } , { <. <. Y , Y >. , { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } >. } >. ) )
11 10 simpld 
 |-  ( ph -> X e. A )
12 2 4 5 termcbas2 
 |-  ( ph -> B = { Y } )
13 12 xpeq1d 
 |-  ( ph -> ( B X. { X } ) = ( { Y } X. { X } ) )
14 xpsng 
 |-  ( ( Y e. B /\ X e. A ) -> ( { Y } X. { X } ) = { <. Y , X >. } )
15 5 11 14 syl2anc 
 |-  ( ph -> ( { Y } X. { X } ) = { <. Y , X >. } )
16 13 15 eqtrd 
 |-  ( ph -> ( B X. { X } ) = { <. Y , X >. } )
17 12 adantr 
 |-  ( ( ph /\ y e. B ) -> B = { Y } )
18 2 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> D e. TermCat )
19 simprl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> y e. B )
20 simprr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> z e. B )
21 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
22 5 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> Y e. B )
23 18 4 19 20 21 9 22 termchom2 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( Hom ` D ) z ) = { ( ( Id ` D ) ` Y ) } )
24 23 xpeq1d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( y ( Hom ` D ) z ) X. { ( ( Id ` C ) ` X ) } ) = ( { ( ( Id ` D ) ` Y ) } X. { ( ( Id ` C ) ` X ) } ) )
25 fvex 
 |-  ( ( Id ` D ) ` Y ) e. _V
26 fvex 
 |-  ( ( Id ` C ) ` X ) e. _V
27 25 26 xpsn 
 |-  ( { ( ( Id ` D ) ` Y ) } X. { ( ( Id ` C ) ` X ) } ) = { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. }
28 24 27 eqtrdi 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( y ( Hom ` D ) z ) X. { ( ( Id ` C ) ` X ) } ) = { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } )
29 12 17 28 mpoeq123dva 
 |-  ( ph -> ( y e. B , z e. B |-> ( ( y ( Hom ` D ) z ) X. { ( ( Id ` C ) ` X ) } ) ) = ( y e. { Y } , z e. { Y } |-> { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } ) )
30 snex 
 |-  { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } e. _V
31 30 a1i 
 |-  ( ph -> { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } e. _V )
32 eqid 
 |-  ( y e. { Y } , z e. { Y } |-> { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } ) = ( y e. { Y } , z e. { Y } |-> { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } )
33 eqidd 
 |-  ( y = Y -> { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } = { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } )
34 eqidd 
 |-  ( z = Y -> { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } = { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } )
35 32 33 34 mposn 
 |-  ( ( Y e. B /\ Y e. B /\ { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } e. _V ) -> ( y e. { Y } , z e. { Y } |-> { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } ) = { <. <. Y , Y >. , { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } >. } )
36 5 5 31 35 syl3anc 
 |-  ( ph -> ( y e. { Y } , z e. { Y } |-> { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } ) = { <. <. Y , Y >. , { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } >. } )
37 29 36 eqtrd 
 |-  ( ph -> ( y e. B , z e. B |-> ( ( y ( Hom ` D ) z ) X. { ( ( Id ` C ) ` X ) } ) ) = { <. <. Y , Y >. , { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } >. } )
38 16 37 opeq12d 
 |-  ( ph -> <. ( B X. { X } ) , ( y e. B , z e. B |-> ( ( y ( Hom ` D ) z ) X. { ( ( Id ` C ) ` X ) } ) ) >. = <. { <. Y , X >. } , { <. <. Y , Y >. , { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } >. } >. )
39 3 func1st2nd 
 |-  ( ph -> ( 1st ` K ) ( D Func C ) ( 2nd ` K ) )
40 39 funcrcl3 
 |-  ( ph -> C e. Cat )
41 2 termccd 
 |-  ( ph -> D e. Cat )
42 eqid 
 |-  ( ( 1st ` L ) ` X ) = ( ( 1st ` L ) ` X )
43 7 40 41 1 11 42 4 21 8 diag1a 
 |-  ( ph -> ( ( 1st ` L ) ` X ) = <. ( B X. { X } ) , ( y e. B , z e. B |-> ( ( y ( Hom ` D ) z ) X. { ( ( Id ` C ) ` X ) } ) ) >. )
44 10 simprd 
 |-  ( ph -> K = <. { <. Y , X >. } , { <. <. Y , Y >. , { <. ( ( Id ` D ) ` Y ) , ( ( Id ` C ) ` X ) >. } >. } >. )
45 38 43 44 3eqtr4rd 
 |-  ( ph -> K = ( ( 1st ` L ) ` X ) )
46 11 45 jca 
 |-  ( ph -> ( X e. A /\ K = ( ( 1st ` L ) ` X ) ) )