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=BaseC
isinitoi.h H=HomC
isinitoi.c φCCat
Assertion isinitoi φOInitOCOBbB∃!hhOHb

Proof

Step Hyp Ref Expression
1 isinitoi.b B=BaseC
2 isinitoi.h H=HomC
3 isinitoi.c φCCat
4 3 1 2 initoval φInitOC=aB|bB∃!hhaHb
5 4 eleq2d φOInitOCOaB|bB∃!hhaHb
6 elrabi OaB|bB∃!hhaHbOB
7 5 6 syl6bi φOInitOCOB
8 7 imp φOInitOCOB
9 3 adantr φOBCCat
10 simpr φOBOB
11 1 2 9 10 isinito φOBOInitOCbB∃!hhOHb
12 11 biimpd φOBOInitOCbB∃!hhOHb
13 12 impancom φOInitOCOBbB∃!hhOHb
14 8 13 jcai φOInitOCOBbB∃!hhOHb