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

Metamath Proof Explorer

Theorem termcbasmo

Description: Two objects in a terminal category are identical. (Contributed by Zhi Wang, 16-Oct-2025)

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

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 termcbasmo.y 
 |-  ( ph -> Y e. B )
5 eqeq1 
 |-  ( x = X -> ( x = y <-> X = y ) )
6 eqeq2 
 |-  ( y = Y -> ( X = y <-> X = Y ) )
7 1 2 termcbas 
 |-  ( ph -> E. z B = { z } )
8 mosn 
 |-  ( B = { z } -> E* x x e. B )
9 8 exlimiv 
 |-  ( E. z B = { z } -> E* x x e. B )
10 7 9 syl 
 |-  ( ph -> E* x x e. B )
11 moel 
 |-  ( E* x x e. B <-> A. x e. B A. y e. B x = y )
12 10 11 sylib 
 |-  ( ph -> A. x e. B A. y e. B x = y )
13 5 6 12 3 4 rspc2dv 
 |-  ( ph -> X = Y )