Metamath Proof Explorer

Theorem diag1f1

Description: The object part of the diagonal functor is 1-1 if B is non-empty. (Contributed by Zhi Wang, 19-Oct-2025)

Ref Expression
Hypotheses diag1f1.l 
|- L = ( C DiagFunc D )
diag1f1.c 
|- ( ph -> C e. Cat )
diag1f1.d 
|- ( ph -> D e. Cat )
diag1f1.a 
|- A = ( Base ` C )
diag1f1.b 
|- B = ( Base ` D )
diag1f1.0 
|- ( ph -> B =/= (/) )
Assertion diag1f1 
|- ( ph -> ( 1st ` L ) : A -1-1-> ( D Func C ) )

Proof

Step Hyp Ref Expression
1 diag1f1.l 
 |-  L = ( C DiagFunc D )
2 diag1f1.c 
 |-  ( ph -> C e. Cat )
3 diag1f1.d 
 |-  ( ph -> D e. Cat )
4 diag1f1.a 
 |-  A = ( Base ` C )
5 diag1f1.b 
 |-  B = ( Base ` D )
6 diag1f1.0 
 |-  ( ph -> B =/= (/) )
7 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
8 7 fucbas 
 |-  ( D Func C ) = ( Base ` ( D FuncCat C ) )
9 1 2 3 7 diagcl 
 |-  ( ph -> L e. ( C Func ( D FuncCat C ) ) )
10 9 func1st2nd 
 |-  ( ph -> ( 1st ` L ) ( C Func ( D FuncCat C ) ) ( 2nd ` L ) )
11 4 8 10 funcf1 
 |-  ( ph -> ( 1st ` L ) : A --> ( D Func C ) )
12 2 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> C e. Cat )
13 3 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> D e. Cat )
14 6 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> B =/= (/) )
15 simprl 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> x e. A )
16 simprr 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> y e. A )
17 eqid 
 |-  ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` x )
18 eqid 
 |-  ( ( 1st ` L ) ` y ) = ( ( 1st ` L ) ` y )
19 1 12 13 4 5 14 15 16 17 18 diag1f1lem 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` y ) -> x = y ) )
20 19 ralrimivva 
 |-  ( ph -> A. x e. A A. y e. A ( ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` y ) -> x = y ) )
21 dff13 
 |-  ( ( 1st ` L ) : A -1-1-> ( D Func C ) <-> ( ( 1st ` L ) : A --> ( D Func C ) /\ A. x e. A A. y e. A ( ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` y ) -> x = y ) ) )
22 11 20 21 sylanbrc 
 |-  ( ph -> ( 1st ` L ) : A -1-1-> ( D Func C ) )