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

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 . See dfinito4 for an alternate definition using the universal property. (Contributed by AV, 3-Apr-2020)

Ref Expression
Assertion df-inito InitO = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cinito ⊢ InitO
1 vc ⊢ 𝑐
2 ccat ⊢ Cat
3 va ⊢ 𝑎
4 cbs ⊢ Base
5 1 cv ⊢ 𝑐
6 5 4 cfv ⊢ ( Base ‘ 𝑐 )
7 vb ⊢ 𝑏
8 vh ⊢ ℎ
9 8 cv ⊢ ℎ
10 3 cv ⊢ 𝑎
11 chom ⊢ Hom
12 5 11 cfv ⊢ ( Hom ‘ 𝑐 )
13 7 cv ⊢ 𝑏
14 10 13 12 co ⊢ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 )
15 9 14 wcel ⊢ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 )
16 15 8 weu ⊢ ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 )
17 16 7 6 wral ⊢ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 )
18 17 3 6 crab ⊢ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) }
19 1 2 18 cmpt ⊢ ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } )
20 0 19 wceq ⊢ InitO = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } )