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	No typesetting found for \|- ( ph -> C e. TermCat ) with typecode \|-
	termcbas.b	$⊢ B = {Base}_{C}$
	termcbasmo.x	$⊢ φ \to X \in B$
Assertion	termcbas2	$⊢ φ \to B = \{X\}$

Step	Hyp	Ref	Expression
1		termcbas.c	Could not format ( ph -> C e. TermCat ) : No typesetting found for \|- ( ph -> C e. TermCat ) with typecode \|-
2		termcbas.b	$⊢ B = {Base}_{C}$
3		termcbasmo.x	$⊢ φ \to X \in B$
4	1 2	termcbas	$⊢ φ \to \exists x B = \{x\}$
5		simpr	$⊢ (φ \land B = \{x\}) \to B = \{x\}$
6	3	adantr	$⊢ (φ \land B = \{x\}) \to X \in B$
7	6 5	eleqtrd	$⊢ (φ \land B = \{x\}) \to X \in \{x\}$
8		elsni	$⊢ X \in \{x\} \to X = x$
9	8	sneqd	$⊢ X \in \{x\} \to \{X\} = \{x\}$
10	7 9	syl	$⊢ (φ \land B = \{x\}) \to \{X\} = \{x\}$
11	5 10	eqtr4d	$⊢ (φ \land B = \{x\}) \to B = \{X\}$
12	4 11	exlimddv	$⊢ φ \to B = \{X\}$

Metamath Proof Explorer