functermc

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

	Ref	Expression
Hypotheses	functermc.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	functermc.e	⊢ ( 𝜑 → 𝐸 ∈ TermCat )
	functermc.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	functermc.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
	functermc.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	functermc.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
	functermc.f	⊢ 𝐹 = ( 𝐵 × 𝐶 )
	functermc.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
Assertion	functermc	⊢ ( 𝜑 → ( 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 ↔ ( 𝐾 = 𝐹 ∧ 𝐿 = 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		functermc.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
2		functermc.e	⊢ ( 𝜑 → 𝐸 ∈ TermCat )
3		functermc.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
4		functermc.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
5		functermc.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
6		functermc.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
7		functermc.f	⊢ 𝐹 = ( 𝐵 × 𝐶 )
8		functermc.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
9		simpr	⊢ ( ( 𝜑 ∧ 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 ) → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
10	3 4 9	funcf1	⊢ ( ( 𝜑 ∧ 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 ) → 𝐾 : 𝐵 ⟶ 𝐶 )
11	2 4	termcbas	⊢ ( 𝜑 → ∃ 𝑧 𝐶 = { 𝑧 } )
12		feq3	⊢ ( 𝐶 = { 𝑧 } → ( 𝐾 : 𝐵 ⟶ 𝐶 ↔ 𝐾 : 𝐵 ⟶ { 𝑧 } ) )
13		vex	⊢ 𝑧 ∈ V
14	13	fconst2	⊢ ( 𝐾 : 𝐵 ⟶ { 𝑧 } ↔ 𝐾 = ( 𝐵 × { 𝑧 } ) )
15		xpeq2	⊢ ( 𝐶 = { 𝑧 } → ( 𝐵 × 𝐶 ) = ( 𝐵 × { 𝑧 } ) )
16	7 15	eqtrid	⊢ ( 𝐶 = { 𝑧 } → 𝐹 = ( 𝐵 × { 𝑧 } ) )
17	16	eqeq2d	⊢ ( 𝐶 = { 𝑧 } → ( 𝐾 = 𝐹 ↔ 𝐾 = ( 𝐵 × { 𝑧 } ) ) )
18	14 17	bitr4id	⊢ ( 𝐶 = { 𝑧 } → ( 𝐾 : 𝐵 ⟶ { 𝑧 } ↔ 𝐾 = 𝐹 ) )
19	12 18	bitrd	⊢ ( 𝐶 = { 𝑧 } → ( 𝐾 : 𝐵 ⟶ 𝐶 ↔ 𝐾 = 𝐹 ) )
20	19	exlimiv	⊢ ( ∃ 𝑧 𝐶 = { 𝑧 } → ( 𝐾 : 𝐵 ⟶ 𝐶 ↔ 𝐾 = 𝐹 ) )
21	11 20	syl	⊢ ( 𝜑 → ( 𝐾 : 𝐵 ⟶ 𝐶 ↔ 𝐾 = 𝐹 ) )
22	21	biimpa	⊢ ( ( 𝜑 ∧ 𝐾 : 𝐵 ⟶ 𝐶 ) → 𝐾 = 𝐹 )
23	10 22	syldan	⊢ ( ( 𝜑 ∧ 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 ) → 𝐾 = 𝐹 )
24	2	termcthind	⊢ ( 𝜑 → 𝐸 ∈ ThinCat )
25	13	fconst	⊢ ( 𝐵 × { 𝑧 } ) : 𝐵 ⟶ { 𝑧 }
26	16	feq1d	⊢ ( 𝐶 = { 𝑧 } → ( 𝐹 : 𝐵 ⟶ 𝐶 ↔ ( 𝐵 × { 𝑧 } ) : 𝐵 ⟶ 𝐶 ) )
27		feq3	⊢ ( 𝐶 = { 𝑧 } → ( ( 𝐵 × { 𝑧 } ) : 𝐵 ⟶ 𝐶 ↔ ( 𝐵 × { 𝑧 } ) : 𝐵 ⟶ { 𝑧 } ) )
28	26 27	bitrd	⊢ ( 𝐶 = { 𝑧 } → ( 𝐹 : 𝐵 ⟶ 𝐶 ↔ ( 𝐵 × { 𝑧 } ) : 𝐵 ⟶ { 𝑧 } ) )
29	25 28	mpbiri	⊢ ( 𝐶 = { 𝑧 } → 𝐹 : 𝐵 ⟶ 𝐶 )
30	29	exlimiv	⊢ ( ∃ 𝑧 𝐶 = { 𝑧 } → 𝐹 : 𝐵 ⟶ 𝐶 )
31	11 30	syl	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
32	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝐸 ∈ TermCat )
33	31	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐶 )
34	33	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐶 )
35	31	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐶 )
36	35	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐶 )
37	32 4 34 36 6	termchomn0	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ¬ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) = ∅ )
38	37	pm2.21d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) = ∅ → ( 𝑧 𝐻 𝑤 ) = ∅ ) )
39	38	ralrimivva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) = ∅ → ( 𝑧 𝐻 𝑤 ) = ∅ ) )
40	3 4 5 6 1 24 31 8 39	functhinc	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐿 ↔ 𝐿 = 𝐺 ) )
41	23 40	functermclem	⊢ ( 𝜑 → ( 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 ↔ ( 𝐾 = 𝐹 ∧ 𝐿 = 𝐺 ) ) )

Metamath Proof Explorer

Theorem functermc

Proof