Metamath Proof Explorer

Theorem 2initoinv

Description: Morphisms between two initial objects are inverses. (Contributed by AV, 14-Apr-2020)

Ref Expression
Hypotheses initoeu1.c 
|- ( ph -> C e. Cat )
initoeu1.a 
|- ( ph -> A e. ( InitO ` C ) )
initoeu1.b 
|- ( ph -> B e. ( InitO ` C ) )
Assertion 2initoinv 
|- ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> F ( A ( Inv ` C ) B ) G )

Proof

Step Hyp Ref Expression
1 initoeu1.c 
 |-  ( ph -> C e. Cat )
2 initoeu1.a 
 |-  ( ph -> A e. ( InitO ` C ) )
3 initoeu1.b 
 |-  ( ph -> B e. ( InitO ` C ) )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
6 eqid 
 |-  ( comp ` C ) = ( comp ` C )
7 1 3ad2ant1 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> C e. Cat )
8 initoo 
 |-  ( C e. Cat -> ( A e. ( InitO ` C ) -> A e. ( Base ` C ) ) )
9 1 2 8 sylc 
 |-  ( ph -> A e. ( Base ` C ) )
10 9 3ad2ant1 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> A e. ( Base ` C ) )
11 initoo 
 |-  ( C e. Cat -> ( B e. ( InitO ` C ) -> B e. ( Base ` C ) ) )
12 1 3 11 sylc 
 |-  ( ph -> B e. ( Base ` C ) )
13 12 3ad2ant1 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> B e. ( Base ` C ) )
14 simp3 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> F e. ( A ( Hom ` C ) B ) )
15 simp2 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> G e. ( B ( Hom ` C ) A ) )
16 4 5 6 7 10 13 10 14 15 catcocl 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( G ( <. A , B >. ( comp ` C ) A ) F ) e. ( A ( Hom ` C ) A ) )
17 4 5 1 initoid 
 |-  ( ( ph /\ A e. ( InitO ` C ) ) -> ( A ( Hom ` C ) A ) = { ( ( Id ` C ) ` A ) } )
18 2 17 mpdan 
 |-  ( ph -> ( A ( Hom ` C ) A ) = { ( ( Id ` C ) ` A ) } )
19 18 3ad2ant1 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( A ( Hom ` C ) A ) = { ( ( Id ` C ) ` A ) } )
20 19 eleq2d 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( ( G ( <. A , B >. ( comp ` C ) A ) F ) e. ( A ( Hom ` C ) A ) <-> ( G ( <. A , B >. ( comp ` C ) A ) F ) e. { ( ( Id ` C ) ` A ) } ) )
21 elsni 
 |-  ( ( G ( <. A , B >. ( comp ` C ) A ) F ) e. { ( ( Id ` C ) ` A ) } -> ( G ( <. A , B >. ( comp ` C ) A ) F ) = ( ( Id ` C ) ` A ) )
22 20 21 syl6bi 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( ( G ( <. A , B >. ( comp ` C ) A ) F ) e. ( A ( Hom ` C ) A ) -> ( G ( <. A , B >. ( comp ` C ) A ) F ) = ( ( Id ` C ) ` A ) ) )
23 16 22 mpd 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( G ( <. A , B >. ( comp ` C ) A ) F ) = ( ( Id ` C ) ` A ) )
24 eqid 
 |-  ( Id ` C ) = ( Id ` C )
25 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
26 4 5 6 24 25 7 10 13 14 15 issect2 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( F ( A ( Sect ` C ) B ) G <-> ( G ( <. A , B >. ( comp ` C ) A ) F ) = ( ( Id ` C ) ` A ) ) )
27 23 26 mpbird 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> F ( A ( Sect ` C ) B ) G )
28 4 5 6 7 13 10 13 15 14 catcocl 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( F ( <. B , A >. ( comp ` C ) B ) G ) e. ( B ( Hom ` C ) B ) )
29 4 5 1 initoid 
 |-  ( ( ph /\ B e. ( InitO ` C ) ) -> ( B ( Hom ` C ) B ) = { ( ( Id ` C ) ` B ) } )
30 3 29 mpdan 
 |-  ( ph -> ( B ( Hom ` C ) B ) = { ( ( Id ` C ) ` B ) } )
31 30 3ad2ant1 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( B ( Hom ` C ) B ) = { ( ( Id ` C ) ` B ) } )
32 31 eleq2d 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( ( F ( <. B , A >. ( comp ` C ) B ) G ) e. ( B ( Hom ` C ) B ) <-> ( F ( <. B , A >. ( comp ` C ) B ) G ) e. { ( ( Id ` C ) ` B ) } ) )
33 elsni 
 |-  ( ( F ( <. B , A >. ( comp ` C ) B ) G ) e. { ( ( Id ` C ) ` B ) } -> ( F ( <. B , A >. ( comp ` C ) B ) G ) = ( ( Id ` C ) ` B ) )
34 32 33 syl6bi 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( ( F ( <. B , A >. ( comp ` C ) B ) G ) e. ( B ( Hom ` C ) B ) -> ( F ( <. B , A >. ( comp ` C ) B ) G ) = ( ( Id ` C ) ` B ) ) )
35 28 34 mpd 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( F ( <. B , A >. ( comp ` C ) B ) G ) = ( ( Id ` C ) ` B ) )
36 4 5 6 24 25 7 13 10 15 14 issect2 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( G ( B ( Sect ` C ) A ) F <-> ( F ( <. B , A >. ( comp ` C ) B ) G ) = ( ( Id ` C ) ` B ) ) )
37 35 36 mpbird 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> G ( B ( Sect ` C ) A ) F )
38 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
39 4 38 1 9 12 25 isinv 
 |-  ( ph -> ( F ( A ( Inv ` C ) B ) G <-> ( F ( A ( Sect ` C ) B ) G /\ G ( B ( Sect ` C ) A ) F ) ) )
40 39 3ad2ant1 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> ( F ( A ( Inv ` C ) B ) G <-> ( F ( A ( Sect ` C ) B ) G /\ G ( B ( Sect ` C ) A ) F ) ) )
41 27 37 40 mpbir2and 
 |-  ( ( ph /\ G e. ( B ( Hom ` C ) A ) /\ F e. ( A ( Hom ` C ) B ) ) -> F ( A ( Inv ` C ) B ) G )