This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐶 ) 𝑌 ) )