termcfunc1eq

Description: Functors with terminal source are equal when they agree on its object. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	termcfunc1eq.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
	termcfunc1eq.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	termcfunc1eq.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	termcfunc1eq.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
	termcfunc1eq.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	termcfunc1eq.e	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) )
Assertion	termcfunc1eq	⊢ ( 𝜑 → 𝐹 = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		termcfunc1eq.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2		termcfunc1eq.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3		termcfunc1eq.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		termcfunc1eq.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
5		termcfunc1eq.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		termcfunc1eq.e	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) )
7	6	opeq2d	⊢ ( 𝜑 → ⟨ 𝑌 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ = ⟨ 𝑌 , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ )
8	7	sneqd	⊢ ( 𝜑 → { ⟨ 𝑌 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ } = { ⟨ 𝑌 , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ } )
9	6	fveq2d	⊢ ( 𝜑 → ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) )
10	9	opeq2d	⊢ ( 𝜑 → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ⟩ = ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ⟩ )
11	10	sneqd	⊢ ( 𝜑 → { ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ⟩ } = { ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ⟩ } )
12	11	opeq2d	⊢ ( 𝜑 → ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ⟩ } ⟩ = ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ⟩ } ⟩ )
13	12	sneqd	⊢ ( 𝜑 → { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ⟩ } ⟩ } = { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ⟩ } ⟩ } )
14	8 13	opeq12d	⊢ ( 𝜑 → ⟨ { ⟨ 𝑌 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ⟩ } ⟩ } ⟩ = ⟨ { ⟨ 𝑌 , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ⟩ } ⟩ } ⟩ )
15		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
16		eqid	⊢ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 )
17		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
18		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
19	15 1 2 3 5 16 17 18	termcfuncval	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) ∧ 𝐹 = ⟨ { ⟨ 𝑌 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ⟩ } ⟩ } ⟩ ) )
20	19	simprd	⊢ ( 𝜑 → 𝐹 = ⟨ { ⟨ 𝑌 , ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ⟩ } ⟩ } ⟩ )
21		eqid	⊢ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 )
22	15 1 4 3 5 21 17 18	termcfuncval	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) ∧ 𝐺 = ⟨ { ⟨ 𝑌 , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ⟩ } ⟩ } ⟩ ) )
23	22	simprd	⊢ ( 𝜑 → 𝐺 = ⟨ { ⟨ 𝑌 , ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑌 ) ) ⟩ } ⟩ } ⟩ )
24	14 20 23	3eqtr4d	⊢ ( 𝜑 → 𝐹 = 𝐺 )

Metamath Proof Explorer

Theorem termcfunc1eq

Proof