This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	No typesetting found for \|- ( ph -> .1. e. TermCat ) with typecode \|-
		isinito4.x	$⊢ φ \to X \in {Base}_{\underset{˙}{1}}$
		isinito4a.f	$⊢ F = 1^{st} (\underset{˙}{1} Δ_{func} C) (X)$
	Assertion	isinito4a	Could not format assertion : No typesetting found for \|- ( ph -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		isinito4.1	Could not format ( ph -> .1. e. TermCat ) : No typesetting found for \|- ( ph -> .1. e. TermCat ) with typecode \|-
2		isinito4.x	$⊢ φ \to X \in {Base}_{\underset{˙}{1}}$
3		isinito4a.f	$⊢ F = 1^{st} (\underset{˙}{1} Δ_{func} C) (X)$
4		initorcl	$⊢ I \in InitO (C) \to C \in Cat$
5	4	anim2i	$⊢ (φ \land I \in InitO (C)) \to (φ \land C \in Cat)$
6		uobrcl	Could not format ( I e. dom ( F ( C UP .1. ) X ) -> ( C e. Cat /\ .1. e. Cat ) ) : No typesetting found for \|- ( I e. dom ( F ( C UP .1. ) X ) -> ( C e. Cat /\ .1. e. Cat ) ) with typecode \|-
7	6	simpld	Could not format ( I e. dom ( F ( C UP .1. ) X ) -> C e. Cat ) : No typesetting found for \|- ( I e. dom ( F ( C UP .1. ) X ) -> C e. Cat ) with typecode \|-
8	7	anim2i	Could not format ( ( ph /\ I e. dom ( F ( C UP .1. ) X ) ) -> ( ph /\ C e. Cat ) ) : No typesetting found for \|- ( ( ph /\ I e. dom ( F ( C UP .1. ) X ) ) -> ( ph /\ C e. Cat ) ) with typecode \|-
9	1	adantr	Could not format ( ( ph /\ C e. Cat ) -> .1. e. TermCat ) : No typesetting found for \|- ( ( ph /\ C e. Cat ) -> .1. e. TermCat ) with typecode \|-
10	2	adantr	$⊢ (φ \land C \in Cat) \to X \in {Base}_{\underset{˙}{1}}$
11		eqid	$⊢ \underset{˙}{1} Δ_{func} C = \underset{˙}{1} Δ_{func} C$
12	9	termccd	$⊢ (φ \land C \in Cat) \to \underset{˙}{1} \in Cat$
13		simpr	$⊢ (φ \land C \in Cat) \to C \in Cat$
14		eqid	$⊢ {Base}_{\underset{˙}{1}} = {Base}_{\underset{˙}{1}}$
15	11 12 13 14 10 3	diag1cl	$⊢ (φ \land C \in Cat) \to F \in (C Func \underset{˙}{1})$
16	9 10 15	isinito4	Could not format ( ( ph /\ C e. Cat ) -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) : No typesetting found for \|- ( ( ph /\ C e. Cat ) -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) with typecode \|-
17	5 8 16	pm5.21nd	Could not format ( ph -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) : No typesetting found for \|- ( ph -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) with typecode \|-