Metamath Proof Explorer

Theorem isinito

Description: The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020)

Ref Expression
Hypotheses isinito.b ⊢ B = Base C
isinito.h ⊢ H = Hom ⁡ C
isinito.c ⊢ φ → C ∈ Cat
isinito.i ⊢ φ → I ∈ B
Assertion isinito ⊢ φ → I ∈ InitO ⁡ C ↔ ∀ b ∈ B ∃! h h ∈ I H b

Proof

Step Hyp Ref Expression
1 isinito.b ⊢ B = Base C
2 isinito.h ⊢ H = Hom ⁡ C
3 isinito.c ⊢ φ → C ∈ Cat
4 isinito.i ⊢ φ → I ∈ B
5 3 1 2 initoval ⊢ φ → InitO ⁡ C = i ∈ B | ∀ b ∈ B ∃! h h ∈ i H b
6 5 eleq2d ⊢ φ → I ∈ InitO ⁡ C ↔ I ∈ i ∈ B | ∀ b ∈ B ∃! h h ∈ i H b
7 oveq1 ⊢ i = I → i H b = I H b
8 7 eleq2d ⊢ i = I → h ∈ i H b ↔ h ∈ I H b
9 8 eubidv ⊢ i = I → ∃! h h ∈ i H b ↔ ∃! h h ∈ I H b
10 9 ralbidv ⊢ i = I → ∀ b ∈ B ∃! h h ∈ i H b ↔ ∀ b ∈ B ∃! h h ∈ I H b
11 10 elrab3 ⊢ I ∈ B → I ∈ i ∈ B | ∀ b ∈ B ∃! h h ∈ i H b ↔ ∀ b ∈ B ∃! h h ∈ I H b
12 4 11 syl ⊢ φ → I ∈ i ∈ B | ∀ b ∈ B ∃! h h ∈ i H b ↔ ∀ b ∈ B ∃! h h ∈ I H b
13 6 12 bitrd ⊢ φ → I ∈ InitO ⁡ C ↔ ∀ b ∈ B ∃! h h ∈ I H b