diag1f1o

Description: The object part of the diagonal functor is a bijection if D is terminal. So any functor from a terminal category is one-to-one correspondent to an object of the target base. (Contributed by Zhi Wang, 21-Oct-2025)

	Ref	Expression
Hypotheses	diag1f1o.a	$⊢ A = {Base}_{C}$
	diag1f1o.d	No typesetting found for \|- ( ph -> D e. TermCat ) with typecode \|-
	diag1f1o.c	$⊢ φ \to C \in Cat$
	diag1f1o.l	$⊢ L = C Δ_{func} D$
Assertion	diag1f1o	$⊢ φ \to 1^{st} (L) : A \underset{1-1 onto}{⟶} D Func C$

Proof

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

Metamath Proof Explorer

Theorem diag1f1o

Proof