functermc

Description: Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025)

	Ref	Expression
Hypotheses	functermc.d	$⊢ φ \to D \in Cat$
	functermc.e	No typesetting found for \|- ( ph -> E e. TermCat ) with typecode \|-
	functermc.b	$⊢ B = {Base}_{D}$
	functermc.c	$⊢ C = {Base}_{E}$
	functermc.h	$⊢ H = Hom (D)$
	functermc.j	$⊢ J = Hom (E)$
	functermc.f	$⊢ F = B \times C$
	functermc.g	$⊢ G = (x \in B, y \in B ⟼ (x H y) \times (F (x) J F (y)))$
Assertion	functermc	$⊢ φ \to (K (D Func E) L \leftrightarrow (K = F \land L = G))$

Proof

Step	Hyp	Ref	Expression
1		functermc.d	$⊢ φ \to D \in Cat$
2		functermc.e	Could not format ( ph -> E e. TermCat ) : No typesetting found for \|- ( ph -> E e. TermCat ) with typecode \|-
3		functermc.b	$⊢ B = {Base}_{D}$
4		functermc.c	$⊢ C = {Base}_{E}$
5		functermc.h	$⊢ H = Hom (D)$
6		functermc.j	$⊢ J = Hom (E)$
7		functermc.f	$⊢ F = B \times C$
8		functermc.g	$⊢ G = (x \in B, y \in B ⟼ (x H y) \times (F (x) J F (y)))$
9		simpr	$⊢ (φ \land K (D Func E) L) \to K (D Func E) L$
10	3 4 9	funcf1	$⊢ (φ \land K (D Func E) L) \to K : B ⟶ C$
11	2 4	termcbas	$⊢ φ \to \exists z C = \{z\}$
12		feq3	$⊢ C = \{z\} \to (K : B ⟶ C \leftrightarrow K : B ⟶ \{z\})$
13		vex	$⊢ z \in V$
14	13	fconst2	$⊢ K : B ⟶ \{z\} \leftrightarrow K = B \times \{z\}$
15		xpeq2	$⊢ C = \{z\} \to B \times C = B \times \{z\}$
16	7 15	eqtrid	$⊢ C = \{z\} \to F = B \times \{z\}$
17	16	eqeq2d	$⊢ C = \{z\} \to (K = F \leftrightarrow K = B \times \{z\})$
18	14 17	bitr4id	$⊢ C = \{z\} \to (K : B ⟶ \{z\} \leftrightarrow K = F)$
19	12 18	bitrd	$⊢ C = \{z\} \to (K : B ⟶ C \leftrightarrow K = F)$
20	19	exlimiv	$⊢ \exists z C = \{z\} \to (K : B ⟶ C \leftrightarrow K = F)$
21	11 20	syl	$⊢ φ \to (K : B ⟶ C \leftrightarrow K = F)$
22	21	biimpa	$⊢ (φ \land K : B ⟶ C) \to K = F$
23	10 22	syldan	$⊢ (φ \land K (D Func E) L) \to K = F$
24	2	termcthind	$⊢ φ \to E \in ThinCat$
25	13	fconst	$⊢ (B \times \{z\}) : B ⟶ \{z\}$
26	16	feq1d	$⊢ C = \{z\} \to (F : B ⟶ C \leftrightarrow (B \times \{z\}) : B ⟶ C)$
27		feq3	$⊢ C = \{z\} \to ((B \times \{z\}) : B ⟶ C \leftrightarrow (B \times \{z\}) : B ⟶ \{z\})$
28	26 27	bitrd	$⊢ C = \{z\} \to (F : B ⟶ C \leftrightarrow (B \times \{z\}) : B ⟶ \{z\})$
29	25 28	mpbiri	$⊢ C = \{z\} \to F : B ⟶ C$
30	29	exlimiv	$⊢ \exists z C = \{z\} \to F : B ⟶ C$
31	11 30	syl	$⊢ φ \to F : B ⟶ C$
32	2	adantr	Could not format ( ( ph /\ ( z e. B /\ w e. B ) ) -> E e. TermCat ) : No typesetting found for \|- ( ( ph /\ ( z e. B /\ w e. B ) ) -> E e. TermCat ) with typecode \|-
33	31	ffvelcdmda	$⊢ (φ \land z \in B) \to F (z) \in C$
34	33	adantrr	$⊢ (φ \land (z \in B \land w \in B)) \to F (z) \in C$
35	31	ffvelcdmda	$⊢ (φ \land w \in B) \to F (w) \in C$
36	35	adantrl	$⊢ (φ \land (z \in B \land w \in B)) \to F (w) \in C$
37	32 4 34 36 6	termchomn0	$⊢ (φ \land (z \in B \land w \in B)) \to \neg F (z) J F (w) = \emptyset$
38	37	pm2.21d	$⊢ (φ \land (z \in B \land w \in B)) \to (F (z) J F (w) = \emptyset \to z H w = \emptyset)$
39	38	ralrimivva	$⊢ φ \to \forall z \in B \forall w \in B (F (z) J F (w) = \emptyset \to z H w = \emptyset)$
40	3 4 5 6 1 24 31 8 39	functhinc	$⊢ φ \to (F (D Func E) L \leftrightarrow L = G)$
41	23 40	functermclem	$⊢ φ \to (K (D Func E) L \leftrightarrow (K = F \land L = G))$

Metamath Proof Explorer

Theorem functermc

Proof