Theorem isinito2

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	⊢ 1 = ( SetCat ‘ 1o )
	isinito2.f	⊢ 𝐹 = ( ( 1st ‘ ( 1 Δfunc 𝐶 ) ) ‘ ∅ )
Assertion	isinito2	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )

Proof

Step	Hyp	Ref	Expression
1		isinito2.1	⊢ 1 = ( SetCat ‘ 1o )
2		isinito2.f	⊢ 𝐹 = ( ( 1st ‘ ( 1 Δfunc 𝐶 ) ) ‘ ∅ )
3		initorcl	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐶 ∈ Cat )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5	4	initoo2	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐼 ∈ ( Base ‘ 𝐶 ) )
6	1 2 3 5	isinito2lem	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ ) )
7	6	ibi	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )
8		id	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )
9	8	up1st2nd	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → 𝐼 ( ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ( 𝐶 UP 1 ) ∅ ) ∅ )
10	9	uprcl2	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → ( 1st ‘ 𝐹 ) ( 𝐶 Func 1 ) ( 2nd ‘ 𝐹 ) )
11	10	funcrcl2	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → 𝐶 ∈ Cat )
12	9 4	uprcl4	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → 𝐼 ∈ ( Base ‘ 𝐶 ) )
13	1 2 11 12	isinito2lem	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ ) )
14	13	ibir	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → 𝐼 ∈ ( InitO ‘ 𝐶 ) )
15	7 14	impbii	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )