termco

Description: The object of a terminal category. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	termcbas.c	No typesetting found for \|- ( ph -> C e. TermCat ) with typecode \|-
	termcbas.b	$⊢ B = {Base}_{C}$
Assertion	termco	$⊢ φ \to ⋃ B \in B$

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	1 2	termcbas	$⊢ φ \to \exists x B = \{x\}$
4		unieq	$⊢ B = \{x\} \to ⋃ B = ⋃ \{x\}$
5		unisnv	$⊢ ⋃ \{x\} = x$
6	4 5	eqtrdi	$⊢ B = \{x\} \to ⋃ B = x$
7		vsnid	$⊢ x \in \{x\}$
8	6 7	eqeltrdi	$⊢ B = \{x\} \to ⋃ B \in \{x\}$
9		id	$⊢ B = \{x\} \to B = \{x\}$
10	8 9	eleqtrrd	$⊢ B = \{x\} \to ⋃ B \in B$
11	10	exlimiv	$⊢ \exists x B = \{x\} \to ⋃ B \in B$
12	3 11	syl	$⊢ φ \to ⋃ B \in B$

Metamath Proof Explorer