Theorem isinito2

Description: The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 23-Oct-2025)

	Ref	Expression
Hypotheses	isinito2.1	$$⊢\underset{\dot{}}{1}=\mathrm{SetCat}\left(1_{𝑜}\right)$$
	isinito2.f	$$⊢F=1^{st}\left(\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C\right)\left(\varnothing \right)$$
Assertion	isinito2	Could not format assertion : No typesetting found for |- ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		isinito2.1	$$⊢\underset{\dot{}}{1}=\mathrm{SetCat}\left(1_{𝑜}\right)$$
2		isinito2.f	$$⊢F=1^{st}\left(\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C\right)\left(\varnothing \right)$$
3		initorcl	$$⊢I\in \mathrm{InitO}\left(C\right)\to C\in \mathrm{Cat}$$
4		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
5	4	initoo2	$$⊢I\in \mathrm{InitO}\left(C\right)\to I\in {\mathrm{Base}}_C$$
6	1 2 3 5	isinito2lem	Could not format ( I e. ( InitO ` C ) -> ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) ) : No typesetting found for |- ( I e. ( InitO ` C ) -> ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) ) with typecode |-
7	6	ibi	Could not format ( I e. ( InitO ` C ) -> I ( F ( C UP .1. ) (/) ) (/) ) : No typesetting found for |- ( I e. ( InitO ` C ) -> I ( F ( C UP .1. ) (/) ) (/) ) with typecode |-
8		id	Could not format ( I ( F ( C UP .1. ) (/) ) (/) -> I ( F ( C UP .1. ) (/) ) (/) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) (/) -> I ( F ( C UP .1. ) (/) ) (/) ) with typecode |-
9	8	up1st2nd	Could not format ( I ( F ( C UP .1. ) (/) ) (/) -> I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) (/) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) (/) -> I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) (/) ) with typecode |-
10	9	uprcl2	Could not format ( I ( F ( C UP .1. ) (/) ) (/) -> ( 1st ` F ) ( C Func .1. ) ( 2nd ` F ) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) (/) -> ( 1st ` F ) ( C Func .1. ) ( 2nd ` F ) ) with typecode |-
11	10	funcrcl2	Could not format ( I ( F ( C UP .1. ) (/) ) (/) -> C e. Cat ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) (/) -> C e. Cat ) with typecode |-
12	9 4	uprcl4	Could not format ( I ( F ( C UP .1. ) (/) ) (/) -> I e. ( Base ` C ) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) (/) -> I e. ( Base ` C ) ) with typecode |-
13	1 2 11 12	isinito2lem	Could not format ( I ( F ( C UP .1. ) (/) ) (/) -> ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) (/) -> ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) ) with typecode |-
14	13	ibir	Could not format ( I ( F ( C UP .1. ) (/) ) (/) -> I e. ( InitO ` C ) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) (/) -> I e. ( InitO ` C ) ) with typecode |-
15	7 14	impbii	Could not format ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) : No typesetting found for |- ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) with typecode |-