Description: An initial object is an object. (Contributed by AV, 14-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | initoo | ⊢ ( 𝐶 ∈ Cat → ( 𝑂 ∈ ( InitO ‘ 𝐶 ) → 𝑂 ∈ ( Base ‘ 𝐶 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 ) | |
2 | eqid | ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) | |
3 | id | ⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ Cat ) | |
4 | 1 2 3 | isinitoi | ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝑂 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑂 ( Hom ‘ 𝐶 ) 𝑏 ) ) ) |
5 | 4 | simpld | ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) → 𝑂 ∈ ( Base ‘ 𝐶 ) ) |
6 | 5 | ex | ⊢ ( 𝐶 ∈ Cat → ( 𝑂 ∈ ( InitO ‘ 𝐶 ) → 𝑂 ∈ ( Base ‘ 𝐶 ) ) ) |