Metamath Proof Explorer

Theorem isinitoi

Description: Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 isinitoi.b ⊢ B = Base C
2 isinitoi.h ⊢ H = Hom ⁡ C
3 isinitoi.c ⊢ φ → C ∈ Cat
4 3 1 2 initoval ⊢ φ → InitO ⁡ C = a ∈ B | ∀ b ∈ B ∃! h h ∈ a H b
5 4 eleq2d ⊢ φ → O ∈ InitO ⁡ C ↔ O ∈ a ∈ B | ∀ b ∈ B ∃! h h ∈ a H b
6 elrabi ⊢ O ∈ a ∈ B | ∀ b ∈ B ∃! h h ∈ a H b → O ∈ B
7 5 6 biimtrdi ⊢ φ → O ∈ InitO ⁡ C → O ∈ B
8 7 imp ⊢ φ ∧ O ∈ InitO ⁡ C → O ∈ B
9 3 adantr ⊢ φ ∧ O ∈ B → C ∈ Cat
10 simpr ⊢ φ ∧ O ∈ B → O ∈ B
11 1 2 9 10 isinito ⊢ φ ∧ O ∈ B → O ∈ InitO ⁡ C ↔ ∀ b ∈ B ∃! h h ∈ O H b
12 11 biimpd ⊢ φ ∧ O ∈ B → O ∈ InitO ⁡ C → ∀ b ∈ B ∃! h h ∈ O H b
13 12 impancom ⊢ φ ∧ O ∈ InitO ⁡ C → O ∈ B → ∀ b ∈ B ∃! h h ∈ O H b
14 8 13 jcai ⊢ φ ∧ O ∈ InitO ⁡ C → O ∈ B ∧ ∀ b ∈ B ∃! h h ∈ O H b