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

Metamath Proof Explorer

Theorem diag2f1lem

Description: Lemma for diag2f1 . The converse is trivial ( fveq2 ). (Contributed by Zhi Wang, 21-Oct-2025)

Ref Expression
Hypotheses diag2f1.l 
|- L = ( C DiagFunc D )
diag2f1.a 
|- A = ( Base ` C )
diag2f1.b 
|- B = ( Base ` D )
diag2f1.h 
|- H = ( Hom ` C )
diag2f1.c 
|- ( ph -> C e. Cat )
diag2f1.d 
|- ( ph -> D e. Cat )
diag2f1.x 
|- ( ph -> X e. A )
diag2f1.y 
|- ( ph -> Y e. A )
diag2f1.0 
|- ( ph -> B =/= (/) )
diag2f1lem.f 
|- ( ph -> F e. ( X H Y ) )
diag2f1lem.g 
|- ( ph -> G e. ( X H Y ) )
Assertion diag2f1lem 
|- ( ph -> ( ( ( X ( 2nd ` L ) Y ) ` F ) = ( ( X ( 2nd ` L ) Y ) ` G ) -> F = G ) )

Proof

Step Hyp Ref Expression
1 diag2f1.l 
 |-  L = ( C DiagFunc D )
2 diag2f1.a 
 |-  A = ( Base ` C )
3 diag2f1.b 
 |-  B = ( Base ` D )
4 diag2f1.h 
 |-  H = ( Hom ` C )
5 diag2f1.c 
 |-  ( ph -> C e. Cat )
6 diag2f1.d 
 |-  ( ph -> D e. Cat )
7 diag2f1.x 
 |-  ( ph -> X e. A )
8 diag2f1.y 
 |-  ( ph -> Y e. A )
9 diag2f1.0 
 |-  ( ph -> B =/= (/) )
10 diag2f1lem.f 
 |-  ( ph -> F e. ( X H Y ) )
11 diag2f1lem.g 
 |-  ( ph -> G e. ( X H Y ) )
12 1 2 3 4 5 6 7 8 10 diag2 
 |-  ( ph -> ( ( X ( 2nd ` L ) Y ) ` F ) = ( B X. { F } ) )
13 1 2 3 4 5 6 7 8 11 diag2 
 |-  ( ph -> ( ( X ( 2nd ` L ) Y ) ` G ) = ( B X. { G } ) )
14 12 13 eqeq12d 
 |-  ( ph -> ( ( ( X ( 2nd ` L ) Y ) ` F ) = ( ( X ( 2nd ` L ) Y ) ` G ) <-> ( B X. { F } ) = ( B X. { G } ) ) )
15 xpcan 
 |-  ( B =/= (/) -> ( ( B X. { F } ) = ( B X. { G } ) <-> { F } = { G } ) )
16 9 15 syl 
 |-  ( ph -> ( ( B X. { F } ) = ( B X. { G } ) <-> { F } = { G } ) )
17 14 16 bitrd 
 |-  ( ph -> ( ( ( X ( 2nd ` L ) Y ) ` F ) = ( ( X ( 2nd ` L ) Y ) ` G ) <-> { F } = { G } ) )
18 sneqrg 
 |-  ( F e. ( X H Y ) -> ( { F } = { G } -> F = G ) )
19 10 18 syl 
 |-  ( ph -> ( { F } = { G } -> F = G ) )
20 17 19 sylbid 
 |-  ( ph -> ( ( ( X ( 2nd ` L ) Y ) ` F ) = ( ( X ( 2nd ` L ) Y ) ` G ) -> F = G ) )