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

Metamath Proof Explorer

Theorem termcbas2

Description: The base of a terminal category is given by its object. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypotheses termcbas.c 
|- ( ph -> C e. TermCat )
termcbas.b 
|- B = ( Base ` C )
termcbasmo.x 
|- ( ph -> X e. B )
Assertion termcbas2 
|- ( ph -> B = { X } )

Proof

Step Hyp Ref Expression
1 termcbas.c 
 |-  ( ph -> C e. TermCat )
2 termcbas.b 
 |-  B = ( Base ` C )
3 termcbasmo.x 
 |-  ( ph -> X e. B )
4 1 2 termcbas 
 |-  ( ph -> E. x B = { x } )
5 simpr 
 |-  ( ( ph /\ B = { x } ) -> B = { x } )
6 3 adantr 
 |-  ( ( ph /\ B = { x } ) -> X e. B )
7 6 5 eleqtrd 
 |-  ( ( ph /\ B = { x } ) -> X e. { x } )
8 elsni 
 |-  ( X e. { x } -> X = x )
9 8 sneqd 
 |-  ( X e. { x } -> { X } = { x } )
10 7 9 syl 
 |-  ( ( ph /\ B = { x } ) -> { X } = { x } )
11 5 10 eqtr4d 
 |-  ( ( ph /\ B = { x } ) -> B = { X } )
12 4 11 exlimddv 
 |-  ( ph -> B = { X } )