Theorem functermc2

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	functermc2	⊢ ( 𝜑 → ( 𝐷 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		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
10	3	fvexi	⊢ 𝐵 ∈ V
11	4	fvexi	⊢ 𝐶 ∈ V
12	10 11	xpex	⊢ ( 𝐵 × 𝐶 ) ∈ V
13	7 12	eqeltri	⊢ 𝐹 ∈ V
14	10 10	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) ∈ V
15	8 14	eqeltri	⊢ 𝐺 ∈ V
16	13 15	relsnop	⊢ Rel { ⟨ 𝐹 , 𝐺 ⟩ }
17	1 2 3 4 5 6 7 8	functermc	⊢ ( 𝜑 → ( 𝑧 ( 𝐷 Func 𝐸 ) 𝑤 ↔ ( 𝑧 = 𝐹 ∧ 𝑤 = 𝐺 ) ) )
18		brsnop	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝑧 { ⟨ 𝐹 , 𝐺 ⟩ } 𝑤 ↔ ( 𝑧 = 𝐹 ∧ 𝑤 = 𝐺 ) ) )
19	13 15 18	mp2an	⊢ ( 𝑧 { ⟨ 𝐹 , 𝐺 ⟩ } 𝑤 ↔ ( 𝑧 = 𝐹 ∧ 𝑤 = 𝐺 ) )
20	17 19	bitr4di	⊢ ( 𝜑 → ( 𝑧 ( 𝐷 Func 𝐸 ) 𝑤 ↔ 𝑧 { ⟨ 𝐹 , 𝐺 ⟩ } 𝑤 ) )
21	9 16 20	eqbrrdiv	⊢ ( 𝜑 → ( 𝐷 Func 𝐸 ) = { ⟨ 𝐹 , 𝐺 ⟩ } )