Metamath Proof Explorer

Theorem diagffth

Description: The diagonal functor is a fully faithful functor from a category C to the category of functors from a terminal category to C . (Contributed by Zhi Wang, 21-Oct-2025)

Ref Expression
Hypotheses diagffth.c 
|- ( ph -> C e. Cat )
diagffth.d 
|- ( ph -> D e. TermCat )
diagffth.q 
|- Q = ( D FuncCat C )
diagffth.l 
|- L = ( C DiagFunc D )
Assertion diagffth 
|- ( ph -> L e. ( ( C Full Q ) i^i ( C Faith Q ) ) )

Proof

Step Hyp Ref Expression
1 diagffth.c 
 |-  ( ph -> C e. Cat )
2 diagffth.d 
 |-  ( ph -> D e. TermCat )
3 diagffth.q 
 |-  Q = ( D FuncCat C )
4 diagffth.l 
 |-  L = ( C DiagFunc D )
5 relfunc 
 |-  Rel ( C Func Q )
6 2 termccd 
 |-  ( ph -> D e. Cat )
7 4 1 6 3 diagcl 
 |-  ( ph -> L e. ( C Func Q ) )
8 1st2nd 
 |-  ( ( Rel ( C Func Q ) /\ L e. ( C Func Q ) ) -> L = <. ( 1st ` L ) , ( 2nd ` L ) >. )
9 5 7 8 sylancr 
 |-  ( ph -> L = <. ( 1st ` L ) , ( 2nd ` L ) >. )
10 7 func1st2nd 
 |-  ( ph -> ( 1st ` L ) ( C Func Q ) ( 2nd ` L ) )
11 eqid 
 |-  ( Base ` C ) = ( Base ` C )
12 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
13 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
14 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
15 eqid 
 |-  ( D Nat C ) = ( D Nat C )
16 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> D e. TermCat )
17 1 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> C e. Cat )
18 4 11 12 13 14 15 16 17 diag2f1o 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` L ) y ) : ( x ( Hom ` C ) y ) -1-1-onto-> ( ( ( 1st ` L ) ` x ) ( D Nat C ) ( ( 1st ` L ) ` y ) ) )
19 18 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( 2nd ` L ) y ) : ( x ( Hom ` C ) y ) -1-1-onto-> ( ( ( 1st ` L ) ` x ) ( D Nat C ) ( ( 1st ` L ) ` y ) ) )
20 3 15 fuchom 
 |-  ( D Nat C ) = ( Hom ` Q )
21 11 12 20 isffth2 
 |-  ( ( 1st ` L ) ( ( C Full Q ) i^i ( C Faith Q ) ) ( 2nd ` L ) <-> ( ( 1st ` L ) ( C Func Q ) ( 2nd ` L ) /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( 2nd ` L ) y ) : ( x ( Hom ` C ) y ) -1-1-onto-> ( ( ( 1st ` L ) ` x ) ( D Nat C ) ( ( 1st ` L ) ` y ) ) ) )
22 10 19 21 sylanbrc 
 |-  ( ph -> ( 1st ` L ) ( ( C Full Q ) i^i ( C Faith Q ) ) ( 2nd ` L ) )
23 df-br 
 |-  ( ( 1st ` L ) ( ( C Full Q ) i^i ( C Faith Q ) ) ( 2nd ` L ) <-> <. ( 1st ` L ) , ( 2nd ` L ) >. e. ( ( C Full Q ) i^i ( C Faith Q ) ) )
24 22 23 sylib 
 |-  ( ph -> <. ( 1st ` L ) , ( 2nd ` L ) >. e. ( ( C Full Q ) i^i ( C Faith Q ) ) )
25 9 24 eqeltrd 
 |-  ( ph -> L e. ( ( C Full Q ) i^i ( C Faith Q ) ) )