Theorem mndtcob

Description: Lemma for mndtchom and mndtcco . (Contributed by Zhi Wang, 22-Sep-2024) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mndtcbaseu.c	|- ( ph -> C = ( MndToCat ` M ) )
	mndtcbaseu.m	|- ( ph -> M e. Mnd )
	mndtcbaseu.b	|- ( ph -> B = ( Base ` C ) )
	mndtchom.x	|- ( ph -> X e. B )
Assertion	mndtcob	|- ( ph -> X = M )

Proof

Step	Hyp	Ref	Expression
1		mndtcbaseu.c	|- ( ph -> C = ( MndToCat ` M ) )
2		mndtcbaseu.m	|- ( ph -> M e. Mnd )
3		mndtcbaseu.b	|- ( ph -> B = ( Base ` C ) )
4		mndtchom.x	|- ( ph -> X e. B )
5	1 2 3	mndtcbasval	|- ( ph -> B = { M } )
6	4 5	eleqtrd	|- ( ph -> X e. { M } )
7		elsng	|- ( X e. B -> ( X e. { M } <-> X = M ) )
8	4 7	syl	|- ( ph -> ( X e. { M } <-> X = M ) )
9	6 8	mpbid	|- ( ph -> X = M )