Theorem dfinito4

Description: An alternate definition of df-inito 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	dfinito4	Could not format assertion : No typesetting found for |- InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		initofn	$$⊢\mathrm{InitO}Fn\mathrm{Cat}$$
2		ovex	Could not format ( f ( c UP d ) (/) ) e. _V : No typesetting found for |- ( f ( c UP d ) (/) ) e. _V with typecode |-
3	2	dmex	Could not format dom ( f ( c UP d ) (/) ) e. _V : No typesetting found for |- dom ( f ( c UP d ) (/) ) e. _V with typecode |-
4	3	csbex	Could not format [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) e. _V : No typesetting found for |- [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) e. _V with typecode |-
5	4	csbex	Could not format [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) e. _V : No typesetting found for |- [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) e. _V with typecode |-
6		eqid	Could not format ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) : No typesetting found for |- ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) with typecode |-
7	5 6	fnmpti	Could not format ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) Fn Cat : No typesetting found for |- ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) Fn Cat with typecode |-
8		eqfnfv	Could not format ( ( InitO Fn Cat /\ ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) Fn Cat ) -> ( InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) <-> A. e e. Cat ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) ) : No typesetting found for |- ( ( InitO Fn Cat /\ ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) Fn Cat ) -> ( InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) <-> A. e e. Cat ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) ) with typecode |-
9	1 7 8	mp2an	Could not format ( InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) <-> A. e e. Cat ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) : No typesetting found for |- ( InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) <-> A. e e. Cat ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) with typecode |-
10		eqid	$$⊢\mathrm{SetCat}\left(1_{𝑜}\right)=\mathrm{SetCat}\left(1_{𝑜}\right)$$
11		eqid	$$⊢1^{st}\left(\mathrm{SetCat}\left(1_{𝑜}\right){\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)=1^{st}\left(\mathrm{SetCat}\left(1_{𝑜}\right){\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)$$
12	10 11	isinito3	Could not format ( x e. ( InitO ` e ) <-> x e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) : No typesetting found for |- ( x e. ( InitO ` e ) <-> x e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) with typecode |-
13	12	eqriv	Could not format ( InitO ` e ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) : No typesetting found for |- ( InitO ` e ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) with typecode |-
14		fvex	$$⊢\mathrm{SetCat}\left(1_{𝑜}\right)\in \mathrm{V}$$
15		fvexd	$$⊢d=\mathrm{SetCat}\left(1_{𝑜}\right)\to 1^{st}\left(d{\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)\in \mathrm{V}$$
16		simpl	$$⊢\left(d=\mathrm{SetCat}\left(1_{𝑜}\right)\wedge f=1^{st}\left(d{\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)\right)\to d=\mathrm{SetCat}\left(1_{𝑜}\right)$$
17	16	oveq2d	Could not format ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> ( e UP d ) = ( e UP ( SetCat ` 1o ) ) ) : No typesetting found for |- ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> ( e UP d ) = ( e UP ( SetCat ` 1o ) ) ) with typecode |-
18		simpr	$$⊢\left(d=\mathrm{SetCat}\left(1_{𝑜}\right)\wedge f=1^{st}\left(d{\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)\right)\to f=1^{st}\left(d{\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)$$
19	16	fvoveq1d	$$⊢\left(d=\mathrm{SetCat}\left(1_{𝑜}\right)\wedge f=1^{st}\left(d{\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)\right)\to 1^{st}\left(d{\Delta }_{\mathrm{func}}e\right)=1^{st}\left(\mathrm{SetCat}\left(1_{𝑜}\right){\Delta }_{\mathrm{func}}e\right)$$
20	19	fveq1d	$$⊢\left(d=\mathrm{SetCat}\left(1_{𝑜}\right)\wedge f=1^{st}\left(d{\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)\right)\to 1^{st}\left(d{\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)=1^{st}\left(\mathrm{SetCat}\left(1_{𝑜}\right){\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)$$
21	18 20	eqtrd	$$⊢\left(d=\mathrm{SetCat}\left(1_{𝑜}\right)\wedge f=1^{st}\left(d{\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)\right)\to f=1^{st}\left(\mathrm{SetCat}\left(1_{𝑜}\right){\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)$$
22		eqidd	$$⊢\left(d=\mathrm{SetCat}\left(1_{𝑜}\right)\wedge f=1^{st}\left(d{\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)\right)\to \varnothing =\varnothing$$
23	17 21 22	oveq123d	Could not format ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> ( f ( e UP d ) (/) ) = ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) : No typesetting found for |- ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> ( f ( e UP d ) (/) ) = ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) with typecode |-
24	23	dmeqd	Could not format ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) : No typesetting found for |- ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) with typecode |-
25	15 24	csbied	Could not format ( d = ( SetCat ` 1o ) -> [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) : No typesetting found for |- ( d = ( SetCat ` 1o ) -> [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) with typecode |-
26	14 25	csbie	Could not format [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) : No typesetting found for |- [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) with typecode |-
27	13 26	eqtr4i	Could not format ( InitO ` e ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) : No typesetting found for |- ( InitO ` e ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) with typecode |-
28		oveq2	$$⊢c=e\to d{\Delta }_{\mathrm{func}}c=d{\Delta }_{\mathrm{func}}e$$
29	28	fveq2d	$$⊢c=e\to 1^{st}\left(d{\Delta }_{\mathrm{func}}c\right)=1^{st}\left(d{\Delta }_{\mathrm{func}}e\right)$$
30	29	fveq1d	$$⊢c=e\to 1^{st}\left(d{\Delta }_{\mathrm{func}}c\right)\left(\varnothing \right)=1^{st}\left(d{\Delta }_{\mathrm{func}}e\right)\left(\varnothing \right)$$
31		oveq1	Could not format ( c = e -> ( c UP d ) = ( e UP d ) ) : No typesetting found for |- ( c = e -> ( c UP d ) = ( e UP d ) ) with typecode |-
32	31	oveqd	Could not format ( c = e -> ( f ( c UP d ) (/) ) = ( f ( e UP d ) (/) ) ) : No typesetting found for |- ( c = e -> ( f ( c UP d ) (/) ) = ( f ( e UP d ) (/) ) ) with typecode |-
33	32	dmeqd	Could not format ( c = e -> dom ( f ( c UP d ) (/) ) = dom ( f ( e UP d ) (/) ) ) : No typesetting found for |- ( c = e -> dom ( f ( c UP d ) (/) ) = dom ( f ( e UP d ) (/) ) ) with typecode |-
34	30 33	csbeq12dv	Could not format ( c = e -> [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) = [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) ) : No typesetting found for |- ( c = e -> [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) = [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) ) with typecode |-
35	34	csbeq2dv	Could not format ( c = e -> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) ) : No typesetting found for |- ( c = e -> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) ) with typecode |-
36		ovex	Could not format ( f ( e UP d ) (/) ) e. _V : No typesetting found for |- ( f ( e UP d ) (/) ) e. _V with typecode |-
37	36	dmex	Could not format dom ( f ( e UP d ) (/) ) e. _V : No typesetting found for |- dom ( f ( e UP d ) (/) ) e. _V with typecode |-
38	37	csbex	Could not format [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) e. _V : No typesetting found for |- [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) e. _V with typecode |-
39	38	csbex	Could not format [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) e. _V : No typesetting found for |- [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) e. _V with typecode |-
40	35 6 39	fvmpt	Could not format ( e e. Cat -> ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) ) : No typesetting found for |- ( e e. Cat -> ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) ) with typecode |-
41	27 40	eqtr4id	Could not format ( e e. Cat -> ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) : No typesetting found for |- ( e e. Cat -> ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) with typecode |-
42	9 41	mprgbir	Could not format InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) : No typesetting found for |- InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) with typecode |-