isinito2lem

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)$
	isinito2lem.c	$⊢ φ \to C \in Cat$
	isinito2lem.i	$⊢ φ \to I \in {Base}_{C}$
Assertion	isinito2lem	Could not format assertion : No typesetting found for \|- ( ph -> ( I e. ( InitO ` C ) <-> I ( 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		isinito2lem.c	$⊢ φ \to C \in Cat$
4		isinito2lem.i	$⊢ φ \to I \in {Base}_{C}$
5		reutru	$⊢ \exists! f f \in (I Hom (C) x) \leftrightarrow \exists! f \in (I Hom (C) x) ⊤$
6		0ex	$⊢ \emptyset \in V$
7		eqeq1	$⊢ y = \emptyset \to (y = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset \leftrightarrow \emptyset = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset)$
8	7	reubidv	$⊢ y = \emptyset \to (\exists! f \in (I Hom (C) x) y = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset \leftrightarrow \exists! f \in (I Hom (C) x) \emptyset = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset)$
9	6 8	ralsn	$⊢ \forall y \in \{\emptyset\} \exists! f \in (I Hom (C) x) y = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset \leftrightarrow \exists! f \in (I Hom (C) x) \emptyset = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset$
10		eqid	$⊢ \underset{˙}{1} Δ_{func} C = \underset{˙}{1} Δ_{func} C$
11		setc1oterm	Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for \|- ( SetCat ` 1o ) e. TermCat with typecode \|-
12	1 11	eqeltri	Could not format .1. e. TermCat : No typesetting found for \|- .1. e. TermCat with typecode \|-
13	12	a1i	Could not format ( ph -> .1. e. TermCat ) : No typesetting found for \|- ( ph -> .1. e. TermCat ) with typecode \|-
14	13	termccatd	$⊢ φ \to \underset{˙}{1} \in Cat$
15	1	setc1obas	$⊢ 1_{𝑜} = {Base}_{\underset{˙}{1}}$
16		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
17	16	a1i	$⊢ φ \to \emptyset \in 1_{𝑜}$
18		eqid	$⊢ {Base}_{C} = {Base}_{C}$
19	10 14 3 15 17 2 18 4	diag11	$⊢ φ \to 1^{st} (F) (I) = \emptyset$
20	19	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (I) = \emptyset$
21	20	opeq2d	$⊢ (φ \land x \in {Base}_{C}) \to ⟨\emptyset, 1^{st} (F) (I)⟩ = ⟨\emptyset, \emptyset⟩$
22	14	adantr	$⊢ (φ \land x \in {Base}_{C}) \to \underset{˙}{1} \in Cat$
23	3	adantr	$⊢ (φ \land x \in {Base}_{C}) \to C \in Cat$
24	16	a1i	$⊢ (φ \land x \in {Base}_{C}) \to \emptyset \in 1_{𝑜}$
25		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
26	10 22 23 15 24 2 18 25	diag11	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (x) = \emptyset$
27	21 26	oveq12d	$⊢ (φ \land x \in {Base}_{C}) \to ⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x) = ⟨\emptyset, \emptyset⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} \emptyset$
28		snex	$⊢ \{⟨\emptyset, \emptyset, \emptyset⟩\} \in V$
29	28	ovsn2	$⊢ ⟨\emptyset, \emptyset⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} \emptyset = \{⟨\emptyset, \emptyset, \emptyset⟩\}$
30	27 29	eqtrdi	$⊢ (φ \land x \in {Base}_{C}) \to ⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x) = \{⟨\emptyset, \emptyset, \emptyset⟩\}$
31	30	adantr	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to ⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x) = \{⟨\emptyset, \emptyset, \emptyset⟩\}$
32	12	a1i	Could not format ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> .1. e. TermCat ) : No typesetting found for \|- ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> .1. e. TermCat ) with typecode \|-
33	32	termccatd	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to \underset{˙}{1} \in Cat$
34	3	ad2antrr	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to C \in Cat$
35	16	a1i	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to \emptyset \in 1_{𝑜}$
36	4	ad2antrr	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to I \in {Base}_{C}$
37		eqid	$⊢ Hom (C) = Hom (C)$
38		eqid	$⊢ Id (\underset{˙}{1}) = Id (\underset{˙}{1})$
39		simplr	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to x \in {Base}_{C}$
40		simpr	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to f \in (I Hom (C) x)$
41	10 33 34 15 35 2 18 36 37 38 39 40	diag12	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to (I 2^{nd} (F) x) (f) = Id (\underset{˙}{1}) (\emptyset)$
42	1 38	setc1oid	$⊢ Id (\underset{˙}{1}) (\emptyset) = \emptyset$
43	41 42	eqtrdi	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to (I 2^{nd} (F) x) (f) = \emptyset$
44		eqidd	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to \emptyset = \emptyset$
45	31 43 44	oveq123d	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset = \emptyset \{⟨\emptyset, \emptyset, \emptyset⟩\} \emptyset$
46	6	ovsn2	$⊢ \emptyset \{⟨\emptyset, \emptyset, \emptyset⟩\} \emptyset = \emptyset$
47	45 46	eqtr2di	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to \emptyset = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset$
48		tbtru	$⊢ \emptyset = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset \leftrightarrow (\emptyset = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset \leftrightarrow ⊤)$
49	47 48	sylib	$⊢ ((φ \land x \in {Base}_{C}) \land f \in (I Hom (C) x)) \to (\emptyset = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset \leftrightarrow ⊤)$
50	49	reubidva	$⊢ (φ \land x \in {Base}_{C}) \to (\exists! f \in (I Hom (C) x) \emptyset = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset \leftrightarrow \exists! f \in (I Hom (C) x) ⊤)$
51	9 50	bitr2id	$⊢ (φ \land x \in {Base}_{C}) \to (\exists! f \in (I Hom (C) x) ⊤ \leftrightarrow \forall y \in \{\emptyset\} \exists! f \in (I Hom (C) x) y = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset)$
52	26	oveq2d	$⊢ (φ \land x \in {Base}_{C}) \to \emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} 1^{st} (F) (x) = \emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} \emptyset$
53		1oex	$⊢ 1_{𝑜} \in V$
54	53	ovsn2	$⊢ \emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} \emptyset = 1_{𝑜}$
55		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
56	54 55	eqtri	$⊢ \emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} \emptyset = \{\emptyset\}$
57	52 56	eqtrdi	$⊢ (φ \land x \in {Base}_{C}) \to \emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} 1^{st} (F) (x) = \{\emptyset\}$
58	57	raleqdv	$⊢ (φ \land x \in {Base}_{C}) \to (\forall y \in (\emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} 1^{st} (F) (x)) \exists! f \in (I Hom (C) x) y = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset \leftrightarrow \forall y \in \{\emptyset\} \exists! f \in (I Hom (C) x) y = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset)$
59	51 58	bitr4d	$⊢ (φ \land x \in {Base}_{C}) \to (\exists! f \in (I Hom (C) x) ⊤ \leftrightarrow \forall y \in (\emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} 1^{st} (F) (x)) \exists! f \in (I Hom (C) x) y = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset)$
60	5 59	bitrid	$⊢ (φ \land x \in {Base}_{C}) \to (\exists! f f \in (I Hom (C) x) \leftrightarrow \forall y \in (\emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} 1^{st} (F) (x)) \exists! f \in (I Hom (C) x) y = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset)$
61	60	ralbidva	$⊢ φ \to (\forall x \in {Base}_{C} \exists! f f \in (I Hom (C) x) \leftrightarrow \forall x \in {Base}_{C} \forall y \in (\emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} 1^{st} (F) (x)) \exists! f \in (I Hom (C) x) y = (I 2^{nd} (F) x) (f) (⟨\emptyset, 1^{st} (F) (I)⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} 1^{st} (F) (x)) \emptyset)$
62	18 37 3 4	isinito	$⊢ φ \to (I \in InitO (C) \leftrightarrow \forall x \in {Base}_{C} \exists! f f \in (I Hom (C) x))$
63	1	setc1ohomfval	$⊢ \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} = Hom (\underset{˙}{1})$
64	1	setc1ocofval	$⊢ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} = comp (\underset{˙}{1})$
65	1 2 3	funcsetc1ocl	$⊢ φ \to F \in (C Func \underset{˙}{1})$
66	65	func1st2nd	$⊢ φ \to 1^{st} (F) (C Func \underset{˙}{1}) 2^{nd} (F)$
67	19	oveq2d	$⊢ φ \to \emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} 1^{st} (F) (I) = \emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} \emptyset$
68	67 54	eqtrdi	$⊢ φ \to \emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} 1^{st} (F) (I) = 1_{𝑜}$
69	16 68	eleqtrrid	$⊢ φ \to \emptyset \in (\emptyset \{⟨\emptyset, \emptyset, 1_{𝑜}⟩\} 1^{st} (F) (I))$
70	18 15 37 63 64 17 66 4 69	isup	Could not format ( ph -> ( I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) (/) <-> A. x e. ( Base ` C ) A. y e. ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` x ) ) E! f e. ( I ( Hom ` C ) x ) y = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) ) ) : No typesetting found for \|- ( ph -> ( I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) (/) <-> A. x e. ( Base ` C ) A. y e. ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` x ) ) E! f e. ( I ( Hom ` C ) x ) y = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) ) ) with typecode \|-
71	61 62 70	3bitr4d	Could not format ( ph -> ( I e. ( InitO ` C ) <-> I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) (/) ) ) : No typesetting found for \|- ( ph -> ( I e. ( InitO ` C ) <-> I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) (/) ) ) with typecode \|-
72	65	up1st2ndb	Could not format ( ph -> ( I ( F ( C UP .1. ) (/) ) (/) <-> I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) (/) ) ) : No typesetting found for \|- ( ph -> ( I ( F ( C UP .1. ) (/) ) (/) <-> I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) (/) ) ) with typecode \|-
73	71 72	bitr4d	Could not format ( ph -> ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) ) : No typesetting found for \|- ( ph -> ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) ) with typecode \|-

Metamath Proof Explorer

Theorem isinito2lem

Proof