Theorem termccisoeu

Description: The isomorphism between terminal categories is unique. (Contributed by Zhi Wang, 26-Oct-2025)

	Ref	Expression
Hypotheses	termcciso.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	termcciso.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	termcciso.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	termcciso.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	termcciso.t	⊢ ( 𝜑 → 𝑋 ∈ TermCat )
	termccisoeu.y	⊢ ( 𝜑 → 𝑌 ∈ TermCat )
Assertion	termccisoeu	⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		termcciso.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		termcciso.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		termcciso.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4		termcciso.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5		termcciso.t	⊢ ( 𝜑 → 𝑋 ∈ TermCat )
6		termccisoeu.y	⊢ ( 𝜑 → 𝑌 ∈ TermCat )
7	1 2	elbasfv	⊢ ( 𝑋 ∈ 𝐵 → 𝑈 ∈ V )
8	3 7	syl	⊢ ( 𝜑 → 𝑈 ∈ V )
9	1	catccat	⊢ ( 𝑈 ∈ V → 𝐶 ∈ Cat )
10	8 9	syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
11	1 2 8	catcbas	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
12	3 11	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ∩ Cat ) )
13	12	elin1d	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
14	1 8 13 5	termcterm	⊢ ( 𝜑 → 𝑋 ∈ ( TermO ‘ 𝐶 ) )
15	4 11	eleqtrd	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑈 ∩ Cat ) )
16	15	elin1d	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
17	1 8 16 6	termcterm	⊢ ( 𝜑 → 𝑌 ∈ ( TermO ‘ 𝐶 ) )
18	10 14 17	termoeu1	⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )