Theorem isinito4a

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 ) )
	isinito4a.f	⊢ 𝐹 = ( ( 1st ‘ ( 1 Δfunc 𝐶 ) ) ‘ 𝑋 )
Assertion	isinito4a	⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isinito4.1	⊢ ( 𝜑 → 1 ∈ TermCat )
2		isinito4.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 1 ) )
3		isinito4a.f	⊢ 𝐹 = ( ( 1st ‘ ( 1 Δfunc 𝐶 ) ) ‘ 𝑋 )
4		initorcl	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐶 ∈ Cat )
5	4	anim2i	⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝜑 ∧ 𝐶 ∈ Cat ) )
6		uobrcl	⊢ ( 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) → ( 𝐶 ∈ Cat ∧ 1 ∈ Cat ) )
7	6	simpld	⊢ ( 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) → 𝐶 ∈ Cat )
8	7	anim2i	⊢ ( ( 𝜑 ∧ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) → ( 𝜑 ∧ 𝐶 ∈ Cat ) )
9	1	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → 1 ∈ TermCat )
10	2	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → 𝑋 ∈ ( Base ‘ 1 ) )
11		eqid	⊢ ( 1 Δfunc 𝐶 ) = ( 1 Δfunc 𝐶 )
12	9	termccatd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → 1 ∈ Cat )
13		simpr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → 𝐶 ∈ Cat )
14		eqid	⊢ ( Base ‘ 1 ) = ( Base ‘ 1 )
15	11 12 13 14 10 3	diag1cl	⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → 𝐹 ∈ ( 𝐶 Func 1 ) )
16	9 10 15	isinito4	⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) )
17	5 8 16	pm5.21nd	⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) )