Metamath Proof Explorer

Definition df-inito

Description: An object A is said to be an initial object provided that for each object B there is exactly one morphism from A to B. Definition 7.1 in Adamek p. 101, or definition in Lang p. 57 (called "a universally repelling object" there). See dfinito2 and dfinito3 for alternate definitions depending on df-termo . (Contributed by AV, 3-Apr-2020)

Ref Expression
Assertion df-inito ⊢ InitO = c ∈ Cat ⟼ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b

Detailed syntax breakdown

Step Hyp Ref Expression
0 cinito class InitO
1 vc setvar c
2 ccat class Cat
3 va setvar a
4 cbs class Base
5 1 cv setvar c
6 5 4 cfv class Base c
7 vb setvar b
8 vh setvar h
9 8 cv setvar h
10 3 cv setvar a
11 chom class Hom
12 5 11 cfv class Hom ⁡ c
13 7 cv setvar b
14 10 13 12 co class a Hom ⁡ c b
15 9 14 wcel wff h ∈ a Hom ⁡ c b
16 15 8 weu wff ∃! h h ∈ a Hom ⁡ c b
17 16 7 6 wral wff ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b
18 17 3 6 crab class a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b
19 1 2 18 cmpt class c ∈ Cat ⟼ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b
20 0 19 wceq wff InitO = c ∈ Cat ⟼ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b