diag2f1lem

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

Step	Hyp	Ref	Expression
1		diag2f1.l	$⊢ L = C Δ_{func} D$
2		diag2f1.a	$⊢ A = {Base}_{C}$
3		diag2f1.b	$⊢ B = {Base}_{D}$
4		diag2f1.h	$⊢ H = Hom (C)$
5		diag2f1.c	$⊢ φ \to C \in Cat$
6		diag2f1.d	$⊢ φ \to D \in Cat$
7		diag2f1.x	$⊢ φ \to X \in A$
8		diag2f1.y	$⊢ φ \to Y \in A$
9		diag2f1.0	$⊢ φ \to B \neq \emptyset$
10		diag2f1lem.f	$⊢ φ \to F \in (X H Y)$
11		diag2f1lem.g	$⊢ φ \to G \in (X H Y)$
12	1 2 3 4 5 6 7 8 10	diag2	$⊢ φ \to (X 2^{nd} (L) Y) (F) = B \times \{F\}$
13	1 2 3 4 5 6 7 8 11	diag2	$⊢ φ \to (X 2^{nd} (L) Y) (G) = B \times \{G\}$
14	12 13	eqeq12d	$⊢ φ \to ((X 2^{nd} (L) Y) (F) = (X 2^{nd} (L) Y) (G) \leftrightarrow B \times \{F\} = B \times \{G\})$
15		xpcan	$⊢ B \neq \emptyset \to (B \times \{F\} = B \times \{G\} \leftrightarrow \{F\} = \{G\})$
16	9 15	syl	$⊢ φ \to (B \times \{F\} = B \times \{G\} \leftrightarrow \{F\} = \{G\})$
17	14 16	bitrd	$⊢ φ \to ((X 2^{nd} (L) Y) (F) = (X 2^{nd} (L) Y) (G) \leftrightarrow \{F\} = \{G\})$
18		sneqrg	$⊢ F \in (X H Y) \to (\{F\} = \{G\} \to F = G)$
19	10 18	syl	$⊢ φ \to (\{F\} = \{G\} \to F = G)$
20	17 19	sylbid	$⊢ φ \to ((X 2^{nd} (L) Y) (F) = (X 2^{nd} (L) Y) (G) \to F = G)$

Metamath Proof Explorer