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	|- ( ph -> .1. e. TermCat )
	isinito4.x	|- ( ph -> X e. ( Base ` .1. ) )
	isinito4a.f	|- F = ( ( 1st ` ( .1. DiagFunc C ) ) ` X )
Assertion	isinito4a	|- ( ph -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) )

Proof

Step	Hyp	Ref	Expression
1		isinito4.1	|- ( ph -> .1. e. TermCat )
2		isinito4.x	|- ( ph -> X e. ( Base ` .1. ) )
3		isinito4a.f	|- F = ( ( 1st ` ( .1. DiagFunc C ) ) ` X )
4		initorcl	|- ( I e. ( InitO ` C ) -> C e. Cat )
5	4	anim2i	|- ( ( ph /\ I e. ( InitO ` C ) ) -> ( ph /\ C e. Cat ) )
6		uobrcl	|- ( I e. dom ( F ( C UP .1. ) X ) -> ( C e. Cat /\ .1. e. Cat ) )
7	6	simpld	|- ( I e. dom ( F ( C UP .1. ) X ) -> C e. Cat )
8	7	anim2i	|- ( ( ph /\ I e. dom ( F ( C UP .1. ) X ) ) -> ( ph /\ C e. Cat ) )
9	1	adantr	|- ( ( ph /\ C e. Cat ) -> .1. e. TermCat )
10	2	adantr	|- ( ( ph /\ C e. Cat ) -> X e. ( Base ` .1. ) )
11		eqid	|- ( .1. DiagFunc C ) = ( .1. DiagFunc C )
12	9	termccd	|- ( ( ph /\ C e. Cat ) -> .1. e. Cat )
13		simpr	|- ( ( ph /\ C e. Cat ) -> C e. Cat )
14		eqid	|- ( Base ` .1. ) = ( Base ` .1. )
15	11 12 13 14 10 3	diag1cl	|- ( ( ph /\ C e. Cat ) -> F e. ( C Func .1. ) )
16	9 10 15	isinito4	|- ( ( ph /\ C e. Cat ) -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) )
17	5 8 16	pm5.21nd	|- ( ph -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) )