This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem diag1f1lem

Description: The object part of the diagonal functor is 1-1 if B is non-empty. Note that ( ph -> ( M = N <-> X = Y ) ) also holds because of diag1f1 and f1fveq . (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 =/= (/) )
diag1f1lem.x 
|- ( ph -> X e. A )
diag1f1lem.y 
|- ( ph -> Y e. A )
diag1f1lem.m 
|- M = ( ( 1st ` L ) ` X )
diag1f1lem.n 
|- N = ( ( 1st ` L ) ` Y )
Assertion diag1f1lem 
|- ( ph -> ( M = N -> X = Y ) )

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 diag1f1lem.x 
 |-  ( ph -> X e. A )
8 diag1f1lem.y 
 |-  ( ph -> Y e. A )
9 diag1f1lem.m 
 |-  M = ( ( 1st ` L ) ` X )
10 diag1f1lem.n 
 |-  N = ( ( 1st ` L ) ` Y )
11 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
12 eqid 
 |-  ( Id ` C ) = ( Id ` C )
13 1 2 3 4 7 9 5 11 12 diag1a 
 |-  ( ph -> M = <. ( B X. { X } ) , ( x e. B , y e. B |-> ( ( x ( Hom ` D ) y ) X. { ( ( Id ` C ) ` X ) } ) ) >. )
14 1 2 3 4 8 10 5 11 12 diag1a 
 |-  ( ph -> N = <. ( B X. { Y } ) , ( x e. B , y e. B |-> ( ( x ( Hom ` D ) y ) X. { ( ( Id ` C ) ` Y ) } ) ) >. )
15 13 14 eqeq12d 
 |-  ( ph -> ( M = N <-> <. ( B X. { X } ) , ( x e. B , y e. B |-> ( ( x ( Hom ` D ) y ) X. { ( ( Id ` C ) ` X ) } ) ) >. = <. ( B X. { Y } ) , ( x e. B , y e. B |-> ( ( x ( Hom ` D ) y ) X. { ( ( Id ` C ) ` Y ) } ) ) >. ) )
16 5 fvexi 
 |-  B e. _V
17 snex 
 |-  { X } e. _V
18 16 17 xpex 
 |-  ( B X. { X } ) e. _V
19 16 16 mpoex 
 |-  ( x e. B , y e. B |-> ( ( x ( Hom ` D ) y ) X. { ( ( Id ` C ) ` X ) } ) ) e. _V
20 18 19 opth1 
 |-  ( <. ( B X. { X } ) , ( x e. B , y e. B |-> ( ( x ( Hom ` D ) y ) X. { ( ( Id ` C ) ` X ) } ) ) >. = <. ( B X. { Y } ) , ( x e. B , y e. B |-> ( ( x ( Hom ` D ) y ) X. { ( ( Id ` C ) ` Y ) } ) ) >. -> ( B X. { X } ) = ( B X. { Y } ) )
21 xpcan 
 |-  ( B =/= (/) -> ( ( B X. { X } ) = ( B X. { Y } ) <-> { X } = { Y } ) )
22 6 21 syl 
 |-  ( ph -> ( ( B X. { X } ) = ( B X. { Y } ) <-> { X } = { Y } ) )
23 sneqrg 
 |-  ( X e. A -> ( { X } = { Y } -> X = Y ) )
24 7 23 syl 
 |-  ( ph -> ( { X } = { Y } -> X = Y ) )
25 22 24 sylbid 
 |-  ( ph -> ( ( B X. { X } ) = ( B X. { Y } ) -> X = Y ) )
26 20 25 syl5 
 |-  ( ph -> ( <. ( B X. { X } ) , ( x e. B , y e. B |-> ( ( x ( Hom ` D ) y ) X. { ( ( Id ` C ) ` X ) } ) ) >. = <. ( B X. { Y } ) , ( x e. B , y e. B |-> ( ( x ( Hom ` D ) y ) X. { ( ( Id ` C ) ` Y ) } ) ) >. -> X = Y ) )
27 15 26 sylbid 
 |-  ( ph -> ( M = N -> X = Y ) )