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

Proof

Step	Hyp	Ref	Expression
1		isinito2.1	⊢ 1 = ( SetCat ‘ 1o )
2		isinito2.f	⊢ 𝐹 = ( ( 1st ‘ ( 1 Δfunc 𝐶 ) ) ‘ ∅ )
3		relup	⊢ Rel ( 𝐹 ( 𝐶 UP 1 ) ∅ )
4	1 2	isinito2	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )
5	4	biimpi	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )
6		releldm	⊢ ( ( Rel ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∧ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ ) → 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) )
7	3 5 6	sylancr	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) )
8		releldmb	⊢ ( Rel ( 𝐹 ( 𝐶 UP 1 ) ∅ ) → ( 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ↔ ∃ 𝑦 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 ) )
9	3 8	ax-mp	⊢ ( 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ↔ ∃ 𝑦 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 )
10		id	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 )
11	10	up1st2nd	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐼 ( ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ( 𝐶 UP 1 ) ∅ ) 𝑦 )
12	1	setc1ohomfval	⊢ { ⟨ ∅ , ∅ , 1o ⟩ } = ( Hom ‘ 1 )
13	11 12	uprcl5	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝑦 ∈ ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ( ( 1st ‘ 𝐹 ) ‘ 𝐼 ) ) )
14		eqid	⊢ ( 1 Δfunc 𝐶 ) = ( 1 Δfunc 𝐶 )
15		setc1oterm	⊢ ( SetCat ‘ 1o ) ∈ TermCat
16	1 15	eqeltri	⊢ 1 ∈ TermCat
17	16	a1i	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 1 ∈ TermCat )
18	17	termccatd	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 1 ∈ Cat )
19	11	uprcl2	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 1 ) ( 2nd ‘ 𝐹 ) )
20	19	funcrcl2	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐶 ∈ Cat )
21	1	setc1obas	⊢ 1o = ( Base ‘ 1 )
22	11 21	uprcl3	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → ∅ ∈ 1o )
23		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
24	11 23	uprcl4	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐼 ∈ ( Base ‘ 𝐶 ) )
25	14 18 20 21 22 2 23 24	diag11	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → ( ( 1st ‘ 𝐹 ) ‘ 𝐼 ) = ∅ )
26	25	oveq2d	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ( ( 1st ‘ 𝐹 ) ‘ 𝐼 ) ) = ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ∅ ) )
27		1oex	⊢ 1o ∈ V
28	27	ovsn2	⊢ ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ∅ ) = 1o
29	26 28	eqtrdi	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ( ( 1st ‘ 𝐹 ) ‘ 𝐼 ) ) = 1o )
30	13 29	eleqtrd	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝑦 ∈ 1o )
31		el1o	⊢ ( 𝑦 ∈ 1o ↔ 𝑦 = ∅ )
32	30 31	sylib	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝑦 = ∅ )
33	10 32	breqtrd	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )
34	33 4	sylibr	⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐼 ∈ ( InitO ‘ 𝐶 ) )
35	34	exlimiv	⊢ ( ∃ 𝑦 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐼 ∈ ( InitO ‘ 𝐶 ) )
36	9 35	sylbi	⊢ ( 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) → 𝐼 ∈ ( InitO ‘ 𝐶 ) )
37	7 36	impbii	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) )