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=BaseC
isinitoi.h ⊢H=Hom⁡C
isinitoi.c ⊢φ→C∈Cat
Assertion istermoi ⊢φ∧O∈TermO⁡C→O∈B∧∀b∈B∃!hh∈bHO

Proof

Step Hyp Ref Expression
1 isinitoi.b ⊢B=BaseC
2 isinitoi.h ⊢H=Hom⁡C
3 isinitoi.c ⊢φ→C∈Cat
4 3 1 2 termoval ⊢φ→TermO⁡C=a∈B|∀b∈B∃!hh∈bHa
5 4 eleq2d ⊢φ→O∈TermO⁡C↔O∈a∈B|∀b∈B∃!hh∈bHa
6 elrabi ⊢O∈a∈B|∀b∈B∃!hh∈bHa→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∃!hh∈bHO
12 11 biimpd ⊢φ∧O∈B→O∈TermO⁡C→∀b∈B∃!hh∈bHO
13 12 impancom ⊢φ∧O∈TermO⁡C→O∈B→∀b∈B∃!hh∈bHO
14 8 13 jcai ⊢φ∧O∈TermO⁡C→O∈B∧∀b∈B∃!hh∈bHO