Theorem isinito4

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}}$$
	isinito4.f	$$⊢\phi \to F\in \left(C\mathrm{Func}\underset{\dot{}}{1}\right)$$
Assertion	isinito4	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		isinito4.f	$$⊢\phi \to F\in \left(C\mathrm{Func}\underset{\dot{}}{1}\right)$$
4		eqid	$$⊢\mathrm{SetCat}\left(1_{𝑜}\right)=\mathrm{SetCat}\left(1_{𝑜}\right)$$
5		eqid	$$⊢1^{st}\left(\mathrm{SetCat}\left(1_{𝑜}\right){\Delta }_{\mathrm{func}}C\right)\left(\varnothing \right)=1^{st}\left(\mathrm{SetCat}\left(1_{𝑜}\right){\Delta }_{\mathrm{func}}C\right)\left(\varnothing \right)$$
6	4 5	isinito3	Could not format ( I e. ( InitO ` C ) <-> I e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) ) : No typesetting found for |- ( I e. ( InitO ` C ) <-> I e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) ) with typecode |-
7	4	setc1obas	$$⊢1_{𝑜}={\mathrm{Base}}_{\mathrm{SetCat}\left(1_{𝑜}\right)}$$
8		eqid	$$⊢{\mathrm{Base}}_{\underset{\dot{}}{1}}={\mathrm{Base}}_{\underset{\dot{}}{1}}$$
9		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
10	9	a1i	$$⊢\phi \to \varnothing \in 1_{𝑜}$$
11	3	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}\underset{\dot{}}{1}\right)2^{nd}\left(F\right)$$
12	11	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
13	4 5 12	funcsetc1ocl	$$⊢\phi \to 1^{st}\left(\mathrm{SetCat}\left(1_{𝑜}\right){\Delta }_{\mathrm{func}}C\right)\left(\varnothing \right)\in \left(C\mathrm{Func}\mathrm{SetCat}\left(1_{𝑜}\right)\right)$$
14		setc1oterm	Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for |- ( SetCat ` 1o ) e. TermCat with typecode |-
15	14	a1i	Could not format ( ph -> ( SetCat ` 1o ) e. TermCat ) : No typesetting found for |- ( ph -> ( SetCat ` 1o ) e. TermCat ) with typecode |-
16	7 8 10 2 13 3 15 1	uobeqterm	Could not format ( ph -> dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) = dom ( F ( C UP .1. ) X ) ) : No typesetting found for |- ( ph -> dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) = dom ( F ( C UP .1. ) X ) ) with typecode |-
17	16	eleq2d	Could not format ( ph -> ( I e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) : No typesetting found for |- ( ph -> ( I e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) with typecode |-
18	6 17	bitrid	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 |-