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 ) )