Metamath Proof Explorer

Theorem termcciso

Description: A category is isomorphic to a terminal category iff it itself is terminal. (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 )
Assertion termcciso 
|- ( ph -> ( Y e. TermCat <-> X ( ~=c ` 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 1 2 elbasfv 
 |-  ( X e. B -> U e. _V )
7 3 6 syl 
 |-  ( ph -> U e. _V )
8 1 catccat 
 |-  ( U e. _V -> C e. Cat )
9 7 8 syl 
 |-  ( ph -> C e. Cat )
10 9 adantr 
 |-  ( ( ph /\ Y e. TermCat ) -> C e. Cat )
11 1 2 7 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 7 13 5 termcterm 
 |-  ( ph -> X e. ( TermO ` C ) )
15 14 adantr 
 |-  ( ( ph /\ Y e. TermCat ) -> X e. ( TermO ` C ) )
16 7 adantr 
 |-  ( ( ph /\ Y e. TermCat ) -> U e. _V )
17 4 adantr 
 |-  ( ( ph /\ Y e. TermCat ) -> Y e. B )
18 11 adantr 
 |-  ( ( ph /\ Y e. TermCat ) -> B = ( U i^i Cat ) )
19 17 18 eleqtrd 
 |-  ( ( ph /\ Y e. TermCat ) -> Y e. ( U i^i Cat ) )
20 19 elin1d 
 |-  ( ( ph /\ Y e. TermCat ) -> Y e. U )
21 simpr 
 |-  ( ( ph /\ Y e. TermCat ) -> Y e. TermCat )
22 1 16 20 21 termcterm 
 |-  ( ( ph /\ Y e. TermCat ) -> Y e. ( TermO ` C ) )
23 10 15 22 termoeu1w 
 |-  ( ( ph /\ Y e. TermCat ) -> X ( ~=c ` C ) Y )
24 13 5 elind 
 |-  ( ph -> X e. ( U i^i TermCat ) )
25 24 ne0d 
 |-  ( ph -> ( U i^i TermCat ) =/= (/) )
26 25 adantr 
 |-  ( ( ph /\ X ( ~=c ` C ) Y ) -> ( U i^i TermCat ) =/= (/) )
27 9 adantr 
 |-  ( ( ph /\ X ( ~=c ` C ) Y ) -> C e. Cat )
28 14 adantr 
 |-  ( ( ph /\ X ( ~=c ` C ) Y ) -> X e. ( TermO ` C ) )
29 simpr 
 |-  ( ( ph /\ X ( ~=c ` C ) Y ) -> X ( ~=c ` C ) Y )
30 27 28 29 termoeu2 
 |-  ( ( ph /\ X ( ~=c ` C ) Y ) -> Y e. ( TermO ` C ) )
31 1 26 30 termcterm2 
 |-  ( ( ph /\ X ( ~=c ` C ) Y ) -> Y e. TermCat )
32 23 31 impbida 
 |-  ( ph -> ( Y e. TermCat <-> X ( ~=c ` C ) Y ) )