Theorem dftermo4

Description: An alternate definition of df-termo using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects . (Contributed by Zhi Wang, 23-Oct-2025)

	Ref	Expression
Assertion	dftermo4	Could not format assertion : No typesetting found for |- TermO = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dftermo2	$$⊢\mathrm{TermO}=\left(c\in \mathrm{Cat}⟼\mathrm{InitO}\left(\mathrm{oppCat}\left(c\right)\right)\right)$$
2		eqid	$$⊢\mathrm{oppCat}\left(c\right)=\mathrm{oppCat}\left(c\right)$$
3	2	oppccat	$$⊢c\in \mathrm{Cat}\to \mathrm{oppCat}\left(c\right)\in \mathrm{Cat}$$
4		ovex	Could not format ( f ( o UP d ) (/) ) e. _V : No typesetting found for |- ( f ( o UP d ) (/) ) e. _V with typecode |-
5	4	dmex	Could not format dom ( f ( o UP d ) (/) ) e. _V : No typesetting found for |- dom ( f ( o UP d ) (/) ) e. _V with typecode |-
6	5	csbex	Could not format [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V : No typesetting found for |- [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V with typecode |-
7	6	csbex	Could not format [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V : No typesetting found for |- [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V with typecode |-
8	7	csbex	Could not format [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V : No typesetting found for |- [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V with typecode |-
9		dfinito4	Could not format InitO = ( o e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) : No typesetting found for |- InitO = ( o e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) with typecode |-
10	9	fvmpts	Could not format ( ( ( oppCat ` c ) e. Cat /\ [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V ) -> ( InitO ` ( oppCat ` c ) ) = [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) : No typesetting found for |- ( ( ( oppCat ` c ) e. Cat /\ [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V ) -> ( InitO ` ( oppCat ` c ) ) = [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) with typecode |-
11	3 8 10	sylancl	Could not format ( c e. Cat -> ( InitO ` ( oppCat ` c ) ) = [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) : No typesetting found for |- ( c e. Cat -> ( InitO ` ( oppCat ` c ) ) = [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) with typecode |-
12	11	mpteq2ia	Could not format ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) ) = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) : No typesetting found for |- ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) ) = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) with typecode |-
13	1 12	eqtri	Could not format TermO = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) : No typesetting found for |- TermO = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) with typecode |-