Metamath Proof Explorer

Theorem istermoi

Description: Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020)

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

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 termoval ⊢ φ → TermO ⁡ C = a ∈ B | ∀ b ∈ B ∃! h h ∈ b H a
5 4 eleq2d ⊢ φ → O ∈ TermO ⁡ C ↔ O ∈ a ∈ B | ∀ b ∈ B ∃! h h ∈ b H a
6 elrabi ⊢ O ∈ a ∈ B | ∀ b ∈ B ∃! h h ∈ b H a → O ∈ B
7 5 6 biimtrdi ⊢ φ → O ∈ TermO ⁡ C → O ∈ B
8 7 imp ⊢ φ ∧ O ∈ TermO ⁡ C → O ∈ B
9 3 adantr ⊢ φ ∧ O ∈ B → C ∈ Cat
10 simpr ⊢ φ ∧ O ∈ B → O ∈ B
11 1 2 9 10 istermo ⊢ φ ∧ O ∈ B → O ∈ TermO ⁡ C ↔ ∀ b ∈ B ∃! h h ∈ b H O
12 11 biimpd ⊢ φ ∧ O ∈ B → O ∈ TermO ⁡ C → ∀ b ∈ B ∃! h h ∈ b H O
13 12 impancom ⊢ φ ∧ O ∈ TermO ⁡ C → O ∈ B → ∀ b ∈ B ∃! h h ∈ b H O
14 8 13 jcai ⊢ φ ∧ O ∈ TermO ⁡ C → O ∈ B ∧ ∀ b ∈ B ∃! h h ∈ b H O