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 
|- C = ( CatCat ` U )
termcciso.b 
|- B = ( Base ` C )
termcciso.x 
|- ( ph -> X e. B )
termcciso.y 
|- ( ph -> Y e. B )
termcciso.t 
|- ( ph -> X e. TermCat )
termccisoeu.y 
|- ( ph -> Y e. TermCat )
Assertion termccisoeu 
|- ( ph -> E! f f e. ( X ( Iso ` C ) Y ) )

Proof

Step Hyp Ref Expression
1 termcciso.c 
 |-  C = ( CatCat ` U )
2 termcciso.b 
 |-  B = ( Base ` C )
3 termcciso.x 
 |-  ( ph -> X e. B )
4 termcciso.y 
 |-  ( ph -> Y e. B )
5 termcciso.t 
 |-  ( ph -> X e. TermCat )
6 termccisoeu.y 
 |-  ( ph -> Y e. TermCat )
7 1 2 elbasfv 
 |-  ( X e. B -> U e. _V )
8 3 7 syl 
 |-  ( ph -> U e. _V )
9 1 catccat 
 |-  ( U e. _V -> C e. Cat )
10 8 9 syl 
 |-  ( ph -> C e. Cat )
11 1 2 8 catcbas 
 |-  ( ph -> B = ( U i^i Cat ) )
12 3 11 eleqtrd 
 |-  ( ph -> X e. ( U i^i Cat ) )
13 12 elin1d 
 |-  ( ph -> X e. U )
14 1 8 13 5 termcterm 
 |-  ( ph -> X e. ( TermO ` C ) )
15 4 11 eleqtrd 
 |-  ( ph -> Y e. ( U i^i Cat ) )
16 15 elin1d 
 |-  ( ph -> Y e. U )
17 1 8 16 6 termcterm 
 |-  ( ph -> Y e. ( TermO ` C ) )
18 10 14 17 termoeu1 
 |-  ( ph -> E! f f e. ( X ( Iso ` C ) Y ) )