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

Metamath Proof Explorer

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	No typesetting found for \|- ( ph -> .1. e. TermCat ) with typecode \|-
		isinito4.x	$⊢ φ \to X \in {Base}_{\underset{˙}{1}}$
		isinito4.f	$⊢ φ \to F \in (C Func \underset{˙}{1})$
	Assertion	isinito4	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		isinito4.f	$⊢ φ \to F \in (C Func \underset{˙}{1})$
4		eqid	$⊢ SetCat (1_{𝑜}) = SetCat (1_{𝑜})$
5		eqid	$⊢ 1^{st} (SetCat (1_{𝑜}) Δ_{func} C) (\emptyset) = 1^{st} (SetCat (1_{𝑜}) Δ_{func} C) (\emptyset)$
6	4 5	isinito3	Could not format ( I e. ( InitO ` C ) <-> I e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) ) : No typesetting found for \|- ( I e. ( InitO ` C ) <-> I e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) ) with typecode \|-
7	4	setc1obas	$⊢ 1_{𝑜} = {Base}_{SetCat (1_{𝑜})}$
8		eqid	$⊢ {Base}_{\underset{˙}{1}} = {Base}_{\underset{˙}{1}}$
9		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
10	9	a1i	$⊢ φ \to \emptyset \in 1_{𝑜}$
11	3	func1st2nd	$⊢ φ \to 1^{st} (F) (C Func \underset{˙}{1}) 2^{nd} (F)$
12	11	funcrcl2	$⊢ φ \to C \in Cat$
13	4 5 12	funcsetc1ocl	$⊢ φ \to 1^{st} (SetCat (1_{𝑜}) Δ_{func} C) (\emptyset) \in (C Func SetCat (1_{𝑜}))$
14		setc1oterm	Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for \|- ( SetCat ` 1o ) e. TermCat with typecode \|-
15	14	a1i	Could not format ( ph -> ( SetCat ` 1o ) e. TermCat ) : No typesetting found for \|- ( ph -> ( SetCat ` 1o ) e. TermCat ) with typecode \|-
16	7 8 10 2 13 3 15 1	uobeqterm	Could not format ( ph -> dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) = dom ( F ( C UP .1. ) X ) ) : No typesetting found for \|- ( ph -> dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) = dom ( F ( C UP .1. ) X ) ) with typecode \|-
17	16	eleq2d	Could not format ( ph -> ( I e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) : No typesetting found for \|- ( ph -> ( I e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) <-> I e. dom ( F ( C UP .1. ) X ) ) ) with typecode \|-
18	6 17	bitrid	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 \|-