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

Metamath Proof Explorer

Theorem termfucterm

Description: All functors between two terminal categories are isomorphisms. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses termfucterm.c 
|- C = ( CatCat ` U )
termfucterm.b 
|- B = ( Base ` C )
termfucterm.i 
|- I = ( Iso ` C )
termfucterm.x 
|- ( ph -> X e. B )
termfucterm.xt 
|- ( ph -> X e. TermCat )
termfucterm.y 
|- ( ph -> Y e. B )
termfucterm.yt 
|- ( ph -> Y e. TermCat )
Assertion termfucterm 
|- ( ph -> ( X Func Y ) = ( X I Y ) )

Proof

Step Hyp Ref Expression
1 termfucterm.c 
 |-  C = ( CatCat ` U )
2 termfucterm.b 
 |-  B = ( Base ` C )
3 termfucterm.i 
 |-  I = ( Iso ` C )
4 termfucterm.x 
 |-  ( ph -> X e. B )
5 termfucterm.xt 
 |-  ( ph -> X e. TermCat )
6 termfucterm.y 
 |-  ( ph -> Y e. B )
7 termfucterm.yt 
 |-  ( ph -> Y e. TermCat )
8 1 2 4 6 5 termcciso 
 |-  ( ph -> ( Y e. TermCat <-> X ( ~=c ` C ) Y ) )
9 7 8 mpbid 
 |-  ( ph -> X ( ~=c ` C ) Y )
10 cicrcl2 
 |-  ( X ( ~=c ` C ) Y -> C e. Cat )
11 9 10 syl 
 |-  ( ph -> C e. Cat )
12 3 2 11 4 6 cic 
 |-  ( ph -> ( X ( ~=c ` C ) Y <-> E. g g e. ( X I Y ) ) )
13 9 12 mpbid 
 |-  ( ph -> E. g g e. ( X I Y ) )
14 13 adantr 
 |-  ( ( ph /\ f e. ( X Func Y ) ) -> E. g g e. ( X I Y ) )
15 eqid 
 |-  ( X FuncCat Y ) = ( X FuncCat Y )
16 5 termccd 
 |-  ( ph -> X e. Cat )
17 15 16 7 fucterm 
 |-  ( ph -> ( X FuncCat Y ) e. TermCat )
18 17 ad2antrr 
 |-  ( ( ( ph /\ f e. ( X Func Y ) ) /\ g e. ( X I Y ) ) -> ( X FuncCat Y ) e. TermCat )
19 15 fucbas 
 |-  ( X Func Y ) = ( Base ` ( X FuncCat Y ) )
20 simplr 
 |-  ( ( ( ph /\ f e. ( X Func Y ) ) /\ g e. ( X I Y ) ) -> f e. ( X Func Y ) )
21 fullfunc 
 |-  ( X Full Y ) C_ ( X Func Y )
22 eqid 
 |-  ( Base ` X ) = ( Base ` X )
23 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
24 simpr 
 |-  ( ( ( ph /\ f e. ( X Func Y ) ) /\ g e. ( X I Y ) ) -> g e. ( X I Y ) )
25 1 22 23 3 24 catcisoi 
 |-  ( ( ( ph /\ f e. ( X Func Y ) ) /\ g e. ( X I Y ) ) -> ( g e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` g ) : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) )
26 25 simpld 
 |-  ( ( ( ph /\ f e. ( X Func Y ) ) /\ g e. ( X I Y ) ) -> g e. ( ( X Full Y ) i^i ( X Faith Y ) ) )
27 26 elin1d 
 |-  ( ( ( ph /\ f e. ( X Func Y ) ) /\ g e. ( X I Y ) ) -> g e. ( X Full Y ) )
28 21 27 sselid 
 |-  ( ( ( ph /\ f e. ( X Func Y ) ) /\ g e. ( X I Y ) ) -> g e. ( X Func Y ) )
29 18 19 20 28 termcbasmo 
 |-  ( ( ( ph /\ f e. ( X Func Y ) ) /\ g e. ( X I Y ) ) -> f = g )
30 29 24 eqeltrd 
 |-  ( ( ( ph /\ f e. ( X Func Y ) ) /\ g e. ( X I Y ) ) -> f e. ( X I Y ) )
31 14 30 exlimddv 
 |-  ( ( ph /\ f e. ( X Func Y ) ) -> f e. ( X I Y ) )
32 simpr 
 |-  ( ( ph /\ f e. ( X I Y ) ) -> f e. ( X I Y ) )
33 1 22 23 3 32 catcisoi 
 |-  ( ( ph /\ f e. ( X I Y ) ) -> ( f e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` f ) : ( Base ` X ) -1-1-onto-> ( Base ` Y ) ) )
34 33 simpld 
 |-  ( ( ph /\ f e. ( X I Y ) ) -> f e. ( ( X Full Y ) i^i ( X Faith Y ) ) )
35 34 elin1d 
 |-  ( ( ph /\ f e. ( X I Y ) ) -> f e. ( X Full Y ) )
36 21 35 sselid 
 |-  ( ( ph /\ f e. ( X I Y ) ) -> f e. ( X Func Y ) )
37 31 36 impbida 
 |-  ( ph -> ( f e. ( X Func Y ) <-> f e. ( X I Y ) ) )
38 37 eqrdv 
 |-  ( ph -> ( X Func Y ) = ( X I Y ) )