Theorem mndtcob

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

	Ref	Expression
Hypotheses	mndtcbaseu.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
	mndtcbaseu.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
	mndtcbaseu.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
	mndtchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	mndtcob	⊢ ( 𝜑 → 𝑋 = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		mndtcbaseu.c	⊢ ( 𝜑 → 𝐶 = ( MndToCat ‘ 𝑀 ) )
2		mndtcbaseu.m	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3		mndtcbaseu.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
4		mndtchom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5	1 2 3	mndtcbasval	⊢ ( 𝜑 → 𝐵 = { 𝑀 } )
6	4 5	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ { 𝑀 } )
7		elsng	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ { 𝑀 } ↔ 𝑋 = 𝑀 ) )
8	4 7	syl	⊢ ( 𝜑 → ( 𝑋 ∈ { 𝑀 } ↔ 𝑋 = 𝑀 ) )
9	6 8	mpbid	⊢ ( 𝜑 → 𝑋 = 𝑀 )