Theorem isinito3

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	isinito3	Could not format assertion : No typesetting found for |- ( I e. ( InitO ` C ) <-> I e. dom ( 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		relup	Could not format Rel ( F ( C UP .1. ) (/) ) : No typesetting found for |- Rel ( F ( C UP .1. ) (/) ) with typecode |-
4	1 2	isinito2	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 |-
5	4	biimpi	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 |-
6		releldm	Could not format ( ( Rel ( F ( C UP .1. ) (/) ) /\ I ( F ( C UP .1. ) (/) ) (/) ) -> I e. dom ( F ( C UP .1. ) (/) ) ) : No typesetting found for |- ( ( Rel ( F ( C UP .1. ) (/) ) /\ I ( F ( C UP .1. ) (/) ) (/) ) -> I e. dom ( F ( C UP .1. ) (/) ) ) with typecode |-
7	3 5 6	sylancr	Could not format ( I e. ( InitO ` C ) -> I e. dom ( F ( C UP .1. ) (/) ) ) : No typesetting found for |- ( I e. ( InitO ` C ) -> I e. dom ( F ( C UP .1. ) (/) ) ) with typecode |-
8		releldmb	Could not format ( Rel ( F ( C UP .1. ) (/) ) -> ( I e. dom ( F ( C UP .1. ) (/) ) <-> E. y I ( F ( C UP .1. ) (/) ) y ) ) : No typesetting found for |- ( Rel ( F ( C UP .1. ) (/) ) -> ( I e. dom ( F ( C UP .1. ) (/) ) <-> E. y I ( F ( C UP .1. ) (/) ) y ) ) with typecode |-
9	3 8	ax-mp	Could not format ( I e. dom ( F ( C UP .1. ) (/) ) <-> E. y I ( F ( C UP .1. ) (/) ) y ) : No typesetting found for |- ( I e. dom ( F ( C UP .1. ) (/) ) <-> E. y I ( F ( C UP .1. ) (/) ) y ) with typecode |-
10		id	Could not format ( I ( F ( C UP .1. ) (/) ) y -> I ( F ( C UP .1. ) (/) ) y ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> I ( F ( C UP .1. ) (/) ) y ) with typecode |-
11	10	up1st2nd	Could not format ( I ( F ( C UP .1. ) (/) ) y -> I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) y ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) y ) with typecode |-
12	1	setc1ohomfval	$$⊢\left\{⟨\varnothing ,\varnothing ,1_{𝑜}⟩\right\}=\mathrm{Hom}\left(\underset{\dot{}}{1}\right)$$
13	11 12	uprcl5	Could not format ( I ( F ( C UP .1. ) (/) ) y -> y e. ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` I ) ) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> y e. ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` I ) ) ) with typecode |-
14		eqid	$$⊢\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C=\underset{\dot{}}{1}{\Delta }_{\mathrm{func}}C$$
15		setc1oterm	Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for |- ( SetCat ` 1o ) e. TermCat with typecode |-
16	1 15	eqeltri	Could not format .1. e. TermCat : No typesetting found for |- .1. e. TermCat with typecode |-
17	16	a1i	Could not format ( I ( F ( C UP .1. ) (/) ) y -> .1. e. TermCat ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> .1. e. TermCat ) with typecode |-
18	17	termccd	Could not format ( I ( F ( C UP .1. ) (/) ) y -> .1. e. Cat ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> .1. e. Cat ) with typecode |-
19	11	uprcl2	Could not format ( I ( F ( C UP .1. ) (/) ) y -> ( 1st ` F ) ( C Func .1. ) ( 2nd ` F ) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> ( 1st ` F ) ( C Func .1. ) ( 2nd ` F ) ) with typecode |-
20	19	funcrcl2	Could not format ( I ( F ( C UP .1. ) (/) ) y -> C e. Cat ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> C e. Cat ) with typecode |-
21	1	setc1obas	$$⊢1_{𝑜}={\mathrm{Base}}_{\underset{\dot{}}{1}}$$
22	11 21	uprcl3	Could not format ( I ( F ( C UP .1. ) (/) ) y -> (/) e. 1o ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> (/) e. 1o ) with typecode |-
23		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
24	11 23	uprcl4	Could not format ( I ( F ( C UP .1. ) (/) ) y -> I e. ( Base ` C ) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> I e. ( Base ` C ) ) with typecode |-
25	14 18 20 21 22 2 23 24	diag11	Could not format ( I ( F ( C UP .1. ) (/) ) y -> ( ( 1st ` F ) ` I ) = (/) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> ( ( 1st ` F ) ` I ) = (/) ) with typecode |-
26	25	oveq2d	Could not format ( I ( F ( C UP .1. ) (/) ) y -> ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` I ) ) = ( (/) { <. (/) , (/) , 1o >. } (/) ) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` I ) ) = ( (/) { <. (/) , (/) , 1o >. } (/) ) ) with typecode |-
27		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
28	27	ovsn2	$$⊢\varnothing \left\{⟨\varnothing ,\varnothing ,1_{𝑜}⟩\right\}\varnothing =1_{𝑜}$$
29	26 28	eqtrdi	Could not format ( I ( F ( C UP .1. ) (/) ) y -> ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` I ) ) = 1o ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` I ) ) = 1o ) with typecode |-
30	13 29	eleqtrd	Could not format ( I ( F ( C UP .1. ) (/) ) y -> y e. 1o ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> y e. 1o ) with typecode |-
31		el1o	$$⊢y\in 1_{𝑜}\leftrightarrow y=\varnothing$$
32	30 31	sylib	Could not format ( I ( F ( C UP .1. ) (/) ) y -> y = (/) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> y = (/) ) with typecode |-
33	10 32	breqtrd	Could not format ( I ( F ( C UP .1. ) (/) ) y -> I ( F ( C UP .1. ) (/) ) (/) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> I ( F ( C UP .1. ) (/) ) (/) ) with typecode |-
34	33 4	sylibr	Could not format ( I ( F ( C UP .1. ) (/) ) y -> I e. ( InitO ` C ) ) : No typesetting found for |- ( I ( F ( C UP .1. ) (/) ) y -> I e. ( InitO ` C ) ) with typecode |-
35	34	exlimiv	Could not format ( E. y I ( F ( C UP .1. ) (/) ) y -> I e. ( InitO ` C ) ) : No typesetting found for |- ( E. y I ( F ( C UP .1. ) (/) ) y -> I e. ( InitO ` C ) ) with typecode |-
36	9 35	sylbi	Could not format ( I e. dom ( F ( C UP .1. ) (/) ) -> I e. ( InitO ` C ) ) : No typesetting found for |- ( I e. dom ( F ( C UP .1. ) (/) ) -> I e. ( InitO ` C ) ) with typecode |-
37	7 36	impbii	Could not format ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) (/) ) ) : No typesetting found for |- ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) (/) ) ) with typecode |-