Metamath Proof Explorer

Theorem initoval

Description: The value of the initial object function, i.e. the set of all initial objects of a category. (Contributed by AV, 3-Apr-2020)

Ref Expression
Hypotheses initoval.c ⊢ φ → C ∈ Cat
initoval.b ⊢ B = Base C
initoval.h ⊢ H = Hom ⁡ C
Assertion initoval ⊢ φ → InitO ⁡ C = a ∈ B | ∀ b ∈ B ∃! h h ∈ a H b

Proof

Step Hyp Ref Expression
1 initoval.c ⊢ φ → C ∈ Cat
2 initoval.b ⊢ B = Base C
3 initoval.h ⊢ H = Hom ⁡ C
4 df-inito ⊢ InitO = c ∈ Cat ⟼ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b
5 fveq2 ⊢ c = C → Base c = Base C
6 5 2 eqtr4di ⊢ c = C → Base c = B
7 fveq2 ⊢ c = C → Hom ⁡ c = Hom ⁡ C
8 7 3 eqtr4di ⊢ c = C → Hom ⁡ c = H
9 8 oveqd ⊢ c = C → a Hom ⁡ c b = a H b
10 9 eleq2d ⊢ c = C → h ∈ a Hom ⁡ c b ↔ h ∈ a H b
11 10 eubidv ⊢ c = C → ∃! h h ∈ a Hom ⁡ c b ↔ ∃! h h ∈ a H b
12 6 11 raleqbidv ⊢ c = C → ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b ↔ ∀ b ∈ B ∃! h h ∈ a H b
13 6 12 rabeqbidv ⊢ c = C → a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b = a ∈ B | ∀ b ∈ B ∃! h h ∈ a H b
14 2 fvexi ⊢ B ∈ V
15 14 rabex ⊢ a ∈ B | ∀ b ∈ B ∃! h h ∈ a H b ∈ V
16 15 a1i ⊢ φ → a ∈ B | ∀ b ∈ B ∃! h h ∈ a H b ∈ V
17 4 13 1 16 fvmptd3 ⊢ φ → InitO ⁡ C = a ∈ B | ∀ b ∈ B ∃! h h ∈ a H b