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 )