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

Metamath Proof Explorer

Theorem termcterm3

Description: In the category of small categories, a terminal object is equivalent to a terminal category. (Contributed by Zhi Wang, 18-Oct-2025)

Ref Expression
Hypotheses termcterm.e 
|- E = ( CatCat ` U )
termcterm3.u 
|- ( ph -> U e. V )
termcterm3.c 
|- ( ph -> C e. U )
termcterm3.1 
|- ( ph -> ( SetCat ` 1o ) e. U )
Assertion termcterm3 
|- ( ph -> ( C e. TermCat <-> C e. ( TermO ` E ) ) )

Proof

Step Hyp Ref Expression
1 termcterm.e 
 |-  E = ( CatCat ` U )
2 termcterm3.u 
 |-  ( ph -> U e. V )
3 termcterm3.c 
 |-  ( ph -> C e. U )
4 termcterm3.1 
 |-  ( ph -> ( SetCat ` 1o ) e. U )
5 2 adantr 
 |-  ( ( ph /\ C e. TermCat ) -> U e. V )
6 3 adantr 
 |-  ( ( ph /\ C e. TermCat ) -> C e. U )
7 simpr 
 |-  ( ( ph /\ C e. TermCat ) -> C e. TermCat )
8 1 5 6 7 termcterm 
 |-  ( ( ph /\ C e. TermCat ) -> C e. ( TermO ` E ) )
9 setc1oterm 
 |-  ( SetCat ` 1o ) e. TermCat
10 9 a1i 
 |-  ( ph -> ( SetCat ` 1o ) e. TermCat )
11 4 10 elind 
 |-  ( ph -> ( SetCat ` 1o ) e. ( U i^i TermCat ) )
12 11 ne0d 
 |-  ( ph -> ( U i^i TermCat ) =/= (/) )
13 12 adantr 
 |-  ( ( ph /\ C e. ( TermO ` E ) ) -> ( U i^i TermCat ) =/= (/) )
14 simpr 
 |-  ( ( ph /\ C e. ( TermO ` E ) ) -> C e. ( TermO ` E ) )
15 1 13 14 termcterm2 
 |-  ( ( ph /\ C e. ( TermO ` E ) ) -> C e. TermCat )
16 8 15 impbida 
 |-  ( ph -> ( C e. TermCat <-> C e. ( TermO ` E ) ) )