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	⊢ ( 𝜑 → 1 ∈ TermCat )
	isinito4.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 1 ) )
	isinito4.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 1 ) )
Assertion	isinito4	⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isinito4.1	⊢ ( 𝜑 → 1 ∈ TermCat )
2		isinito4.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 1 ) )
3		isinito4.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 1 ) )
4		eqid	⊢ ( SetCat ‘ 1o ) = ( SetCat ‘ 1o )
5		eqid	⊢ ( ( 1st ‘ ( ( SetCat ‘ 1o ) Δfunc 𝐶 ) ) ‘ ∅ ) = ( ( 1st ‘ ( ( SetCat ‘ 1o ) Δfunc 𝐶 ) ) ‘ ∅ )
6	4 5	isinito3	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( ( ( 1st ‘ ( ( SetCat ‘ 1o ) Δfunc 𝐶 ) ) ‘ ∅ ) ( 𝐶 UP ( SetCat ‘ 1o ) ) ∅ ) )
7	4	setc1obas	⊢ 1o = ( Base ‘ ( SetCat ‘ 1o ) )
8		eqid	⊢ ( Base ‘ 1 ) = ( Base ‘ 1 )
9		0lt1o	⊢ ∅ ∈ 1o
10	9	a1i	⊢ ( 𝜑 → ∅ ∈ 1o )
11	3	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 1 ) ( 2nd ‘ 𝐹 ) )
12	11	funcrcl2	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13	4 5 12	funcsetc1ocl	⊢ ( 𝜑 → ( ( 1st ‘ ( ( SetCat ‘ 1o ) Δfunc 𝐶 ) ) ‘ ∅ ) ∈ ( 𝐶 Func ( SetCat ‘ 1o ) ) )
14		setc1oterm	⊢ ( SetCat ‘ 1o ) ∈ TermCat
15	14	a1i	⊢ ( 𝜑 → ( SetCat ‘ 1o ) ∈ TermCat )
16	7 8 10 2 13 3 15 1	uobeqterm	⊢ ( 𝜑 → dom ( ( ( 1st ‘ ( ( SetCat ‘ 1o ) Δfunc 𝐶 ) ) ‘ ∅ ) ( 𝐶 UP ( SetCat ‘ 1o ) ) ∅ ) = dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) )
17	16	eleq2d	⊢ ( 𝜑 → ( 𝐼 ∈ dom ( ( ( 1st ‘ ( ( SetCat ‘ 1o ) Δfunc 𝐶 ) ) ‘ ∅ ) ( 𝐶 UP ( SetCat ‘ 1o ) ) ∅ ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) )
18	6 17	bitrid	⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) )