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{˙}{1} = SetCat (1_{𝑜})$
	isinito2.f	$⊢ F = 1^{st} (\underset{˙}{1} Δ_{func} C) (\emptyset)$
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{˙}{1} = SetCat (1_{𝑜})$
2		isinito2.f	$⊢ F = 1^{st} (\underset{˙}{1} Δ_{func} C) (\emptyset)$
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	$⊢ \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} = Hom (\underset{˙}{1})$
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{˙}{1} Δ_{func} C = \underset{˙}{1} Δ_{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_{𝑜} = {Base}_{\underset{˙}{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	$⊢ {Base}_{C} = {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 V$
28	27	ovsn2	$⊢ \emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} \emptyset = 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 = \emptyset$
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 \|-

Metamath Proof Explorer

Theorem isinito3

Proof