diag2f1o

Description: If D is terminal, the morphism part of a diagonal functor is bijective functions from hom-sets into sets of natural transformations. (Contributed by Zhi Wang, 21-Oct-2025)

	Ref	Expression
Hypotheses	diag2f1o.l	$⊢ L = C Δ_{func} D$
	diag2f1o.a	$⊢ A = {Base}_{C}$
	diag2f1o.h	$⊢ H = Hom (C)$
	diag2f1o.x	$⊢ φ \to X \in A$
	diag2f1o.y	$⊢ φ \to Y \in A$
	diag2f1o.n	$⊢ N = D Nat C$
	diag2f1o.d	No typesetting found for \|- ( ph -> D e. TermCat ) with typecode \|-
	diag2f1o.c	$⊢ φ \to C \in Cat$
Assertion	diag2f1o	$⊢ φ \to (X 2^{nd} (L) Y) : X H Y \underset{1-1 onto}{⟶} 1^{st} (L) (X) N 1^{st} (L) (Y)$

Proof

Step	Hyp	Ref	Expression
1		diag2f1o.l	$⊢ L = C Δ_{func} D$
2		diag2f1o.a	$⊢ A = {Base}_{C}$
3		diag2f1o.h	$⊢ H = Hom (C)$
4		diag2f1o.x	$⊢ φ \to X \in A$
5		diag2f1o.y	$⊢ φ \to Y \in A$
6		diag2f1o.n	$⊢ N = D Nat C$
7		diag2f1o.d	Could not format ( ph -> D e. TermCat ) : No typesetting found for \|- ( ph -> D e. TermCat ) with typecode \|-
8		diag2f1o.c	$⊢ φ \to C \in Cat$
9		eqid	$⊢ {Base}_{D} = {Base}_{D}$
10	7	termccd	$⊢ φ \to D \in Cat$
11	9	istermc2	Could not format ( D e. TermCat <-> ( D e. ThinCat /\ E! z z e. ( Base ` D ) ) ) : No typesetting found for \|- ( D e. TermCat <-> ( D e. ThinCat /\ E! z z e. ( Base ` D ) ) ) with typecode \|-
12	7 11	sylib	$⊢ φ \to (D \in ThinCat \land \exists! z z \in {Base}_{D})$
13	12	simprd	$⊢ φ \to \exists! z z \in {Base}_{D}$
14		euex	$⊢ \exists! z z \in {Base}_{D} \to \exists z z \in {Base}_{D}$
15	13 14	syl	$⊢ φ \to \exists z z \in {Base}_{D}$
16		n0	$⊢ {Base}_{D} \neq \emptyset \leftrightarrow \exists z z \in {Base}_{D}$
17	15 16	sylibr	$⊢ φ \to {Base}_{D} \neq \emptyset$
18	1 2 9 3 8 10 4 5 17 6	diag2f1	$⊢ φ \to (X 2^{nd} (L) Y) : X H Y \underset{1-1}{⟶} 1^{st} (L) (X) N 1^{st} (L) (Y)$
19		f1f	$⊢ (X 2^{nd} (L) Y) : X H Y \underset{1-1}{⟶} 1^{st} (L) (X) N 1^{st} (L) (Y) \to (X 2^{nd} (L) Y) : X H Y ⟶ 1^{st} (L) (X) N 1^{st} (L) (Y)$
20	18 19	syl	$⊢ φ \to (X 2^{nd} (L) Y) : X H Y ⟶ 1^{st} (L) (X) N 1^{st} (L) (Y)$
21	7 9	termcbas	$⊢ φ \to \exists z {Base}_{D} = \{z\}$
22	21	adantr	$⊢ (φ \land m \in (1^{st} (L) (X) N 1^{st} (L) (Y))) \to \exists z {Base}_{D} = \{z\}$
23		fveq2	$⊢ f = m (z) \to (X 2^{nd} (L) Y) (f) = (X 2^{nd} (L) Y) (m (z))$
24	23	eqeq2d	$⊢ f = m (z) \to (m = (X 2^{nd} (L) Y) (f) \leftrightarrow m = (X 2^{nd} (L) Y) (m (z)))$
25	4	ad2antrr	$⊢ ((φ \land m \in (1^{st} (L) (X) N 1^{st} (L) (Y))) \land {Base}_{D} = \{z\}) \to X \in A$
26	5	ad2antrr	$⊢ ((φ \land m \in (1^{st} (L) (X) N 1^{st} (L) (Y))) \land {Base}_{D} = \{z\}) \to Y \in A$
27	7	ad2antrr	Could not format ( ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) /\ ( Base ` D ) = { z } ) -> D e. TermCat ) : No typesetting found for \|- ( ( ( ph /\ m e. ( ( ( 1st ` L ) ` X ) N ( ( 1st ` L ) ` Y ) ) ) /\ ( Base ` D ) = { z } ) -> D e. TermCat ) with typecode \|-
28		simplr	$⊢ ((φ \land m \in (1^{st} (L) (X) N 1^{st} (L) (Y))) \land {Base}_{D} = \{z\}) \to m \in (1^{st} (L) (X) N 1^{st} (L) (Y))$
29		vsnid	$⊢ z \in \{z\}$
30		simpr	$⊢ ((φ \land m \in (1^{st} (L) (X) N 1^{st} (L) (Y))) \land {Base}_{D} = \{z\}) \to {Base}_{D} = \{z\}$
31	29 30	eleqtrrid	$⊢ ((φ \land m \in (1^{st} (L) (X) N 1^{st} (L) (Y))) \land {Base}_{D} = \{z\}) \to z \in {Base}_{D}$
32		eqid	$⊢ m (z) = m (z)$
33	1 2 3 25 26 6 27 28 9 31 32	diag2f1olem	$⊢ ((φ \land m \in (1^{st} (L) (X) N 1^{st} (L) (Y))) \land {Base}_{D} = \{z\}) \to (m (z) \in (X H Y) \land m = (X 2^{nd} (L) Y) (m (z)))$
34	33	simpld	$⊢ ((φ \land m \in (1^{st} (L) (X) N 1^{st} (L) (Y))) \land {Base}_{D} = \{z\}) \to m (z) \in (X H Y)$
35	33	simprd	$⊢ ((φ \land m \in (1^{st} (L) (X) N 1^{st} (L) (Y))) \land {Base}_{D} = \{z\}) \to m = (X 2^{nd} (L) Y) (m (z))$
36	24 34 35	rspcedvdw	$⊢ ((φ \land m \in (1^{st} (L) (X) N 1^{st} (L) (Y))) \land {Base}_{D} = \{z\}) \to \exists f \in (X H Y) m = (X 2^{nd} (L) Y) (f)$
37	22 36	exlimddv	$⊢ (φ \land m \in (1^{st} (L) (X) N 1^{st} (L) (Y))) \to \exists f \in (X H Y) m = (X 2^{nd} (L) Y) (f)$
38	37	ralrimiva	$⊢ φ \to \forall m \in (1^{st} (L) (X) N 1^{st} (L) (Y)) \exists f \in (X H Y) m = (X 2^{nd} (L) Y) (f)$
39		dffo3	$⊢ (X 2^{nd} (L) Y) : X H Y \underset{onto}{⟶} 1^{st} (L) (X) N 1^{st} (L) (Y) \leftrightarrow ((X 2^{nd} (L) Y) : X H Y ⟶ 1^{st} (L) (X) N 1^{st} (L) (Y) \land \forall m \in (1^{st} (L) (X) N 1^{st} (L) (Y)) \exists f \in (X H Y) m = (X 2^{nd} (L) Y) (f))$
40	20 38 39	sylanbrc	$⊢ φ \to (X 2^{nd} (L) Y) : X H Y \underset{onto}{⟶} 1^{st} (L) (X) N 1^{st} (L) (Y)$
41		df-f1o	$⊢ (X 2^{nd} (L) Y) : X H Y \underset{1-1 onto}{⟶} 1^{st} (L) (X) N 1^{st} (L) (Y) \leftrightarrow ((X 2^{nd} (L) Y) : X H Y \underset{1-1}{⟶} 1^{st} (L) (X) N 1^{st} (L) (Y) \land (X 2^{nd} (L) Y) : X H Y \underset{onto}{⟶} 1^{st} (L) (X) N 1^{st} (L) (Y))$
42	18 40 41	sylanbrc	$⊢ φ \to (X 2^{nd} (L) Y) : X H Y \underset{1-1 onto}{⟶} 1^{st} (L) (X) N 1^{st} (L) (Y)$

Metamath Proof Explorer

Theorem diag2f1o

Proof