Theorem isinito4a

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

	Ref	Expression
Hypotheses	isinito4.1	No typesetting found for |- ( ph -> .1. e. TermCat ) with typecode |-
	isinito4.x	$$⊢\phi \to X\in {\mathrm{Base}}_{\underset{\dot{}}{1}}$$
	isinito4a.f	$$⊢F=1^{st}\left(\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C\right)\left(X\right)$$
Assertion	isinito4a	Could not format assertion : No typesetting found for |- ( ph -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		isinito4.1	Could not format ( ph -> .1. e. TermCat ) : No typesetting found for |- ( ph -> .1. e. TermCat ) with typecode |-
2		isinito4.x	$$⊢\phi \to X\in {\mathrm{Base}}_{\underset{\dot{}}{1}}$$
3		isinito4a.f	$$⊢F=1^{st}\left(\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C\right)\left(X\right)$$
4		initorcl	$$⊢I\in \mathrm{InitO}\left(C\right)\to C\in \mathrm{Cat}$$
5	4	anim2i	$$⊢\left(\phi \wedge I\in \mathrm{InitO}\left(C\right)\right)\to \left(\phi \wedge C\in \mathrm{Cat}\right)$$
6		uobrcl	Could not format ( I e. dom ( F ( C UP .1. ) X ) -> ( C e. Cat /\ .1. e. Cat ) ) : No typesetting found for |- ( I e. dom ( F ( C UP .1. ) X ) -> ( C e. Cat /\ .1. e. Cat ) ) with typecode |-
7	6	simpld	Could not format ( I e. dom ( F ( C UP .1. ) X ) -> C e. Cat ) : No typesetting found for |- ( I e. dom ( F ( C UP .1. ) X ) -> C e. Cat ) with typecode |-
8	7	anim2i	Could not format ( ( ph /\ I e. dom ( F ( C UP .1. ) X ) ) -> ( ph /\ C e. Cat ) ) : No typesetting found for |- ( ( ph /\ I e. dom ( F ( C UP .1. ) X ) ) -> ( ph /\ C e. Cat ) ) with typecode |-
9	1	adantr	Could not format ( ( ph /\ C e. Cat ) -> .1. e. TermCat ) : No typesetting found for |- ( ( ph /\ C e. Cat ) -> .1. e. TermCat ) with typecode |-
10	2	adantr	$$⊢\left(\phi \wedge C\in \mathrm{Cat}\right)\to X\in {\mathrm{Base}}_{\underset{\dot{}}{1}}$$
11		eqid	$$⊢\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C=\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C$$
12	9	termccd	$$⊢\left(\phi \wedge C\in \mathrm{Cat}\right)\to \underset{\dot{}}{1}\in \mathrm{Cat}$$
13		simpr	$$⊢\left(\phi \wedge C\in \mathrm{Cat}\right)\to C\in \mathrm{Cat}$$
14		eqid	$$⊢{\mathrm{Base}}_{\underset{\dot{}}{1}}={\mathrm{Base}}_{\underset{\dot{}}{1}}$$
15	11 12 13 14 10 3	diag1cl	$$⊢\left(\phi \wedge C\in \mathrm{Cat}\right)\to F\in \left(C\mathrm{Func}\underset{\dot{}}{1}\right)$$
16	9 10 15	isinito4	Could not format ( ( ph /\ C e. Cat ) -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) : No typesetting found for |- ( ( ph /\ C e. Cat ) -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) with typecode |-
17	5 8 16	pm5.21nd	Could not format ( ph -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) : No typesetting found for |- ( ph -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) with typecode |-