This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem initoeu2lem0

Description: Lemma 0 for initoeu2 . (Contributed by AV, 9-Apr-2020)

Ref Expression
Hypotheses initoeu1.c 
|- ( ph -> C e. Cat )
initoeu1.a 
|- ( ph -> A e. ( InitO ` C ) )
initoeu2lem.x 
|- X = ( Base ` C )
initoeu2lem.h 
|- H = ( Hom ` C )
initoeu2lem.i 
|- I = ( Iso ` C )
initoeu2lem.o 
|- .o. = ( comp ` C )
Assertion initoeu2lem0 
|- ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> G = ( F ( <. B , A >. .o. D ) K ) )

Proof

Step Hyp Ref Expression
1 initoeu1.c 
 |-  ( ph -> C e. Cat )
2 initoeu1.a 
 |-  ( ph -> A e. ( InitO ` C ) )
3 initoeu2lem.x 
 |-  X = ( Base ` C )
4 initoeu2lem.h 
 |-  H = ( Hom ` C )
5 initoeu2lem.i 
 |-  I = ( Iso ` C )
6 initoeu2lem.o 
 |-  .o. = ( comp ` C )
7 3simpa 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) )
8 simp3 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) )
9 8 eqcomd 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) )
10 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
11 1 adantr 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) -> C e. Cat )
12 11 adantr 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> C e. Cat )
13 simpr1 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) -> A e. X )
14 13 adantr 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> A e. X )
15 simpr2 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) -> B e. X )
16 15 adantr 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> B e. X )
17 simplr3 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> D e. X )
18 5 oveqi 
 |-  ( B I A ) = ( B ( Iso ` C ) A )
19 18 eleq2i 
 |-  ( K e. ( B I A ) <-> K e. ( B ( Iso ` C ) A ) )
20 19 biimpi 
 |-  ( K e. ( B I A ) -> K e. ( B ( Iso ` C ) A ) )
21 20 3ad2ant1 
 |-  ( ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) -> K e. ( B ( Iso ` C ) A ) )
22 21 adantl 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> K e. ( B ( Iso ` C ) A ) )
23 4 oveqi 
 |-  ( B H D ) = ( B ( Hom ` C ) D )
24 23 eleq2i 
 |-  ( G e. ( B H D ) <-> G e. ( B ( Hom ` C ) D ) )
25 24 biimpi 
 |-  ( G e. ( B H D ) -> G e. ( B ( Hom ` C ) D ) )
26 25 3ad2ant3 
 |-  ( ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) -> G e. ( B ( Hom ` C ) D ) )
27 26 adantl 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> G e. ( B ( Hom ` C ) D ) )
28 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
29 3 28 5 11 15 13 isohom 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) -> ( B I A ) C_ ( B ( Hom ` C ) A ) )
30 29 sseld 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) -> ( K e. ( B I A ) -> K e. ( B ( Hom ` C ) A ) ) )
31 30 com12 
 |-  ( K e. ( B I A ) -> ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) -> K e. ( B ( Hom ` C ) A ) ) )
32 31 3ad2ant1 
 |-  ( ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) -> ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) -> K e. ( B ( Hom ` C ) A ) ) )
33 32 impcom 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> K e. ( B ( Hom ` C ) A ) )
34 4 oveqi 
 |-  ( A H D ) = ( A ( Hom ` C ) D )
35 34 eleq2i 
 |-  ( F e. ( A H D ) <-> F e. ( A ( Hom ` C ) D ) )
36 35 biimpi 
 |-  ( F e. ( A H D ) -> F e. ( A ( Hom ` C ) D ) )
37 36 3ad2ant2 
 |-  ( ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) -> F e. ( A ( Hom ` C ) D ) )
38 37 adantl 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> F e. ( A ( Hom ` C ) D ) )
39 3 28 6 12 16 14 17 33 38 catcocl 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> ( F ( <. B , A >. .o. D ) K ) e. ( B ( Hom ` C ) D ) )
40 eqid 
 |-  ( ( B ( Inv ` C ) A ) ` K ) = ( ( B ( Inv ` C ) A ) ` K )
41 6 oveqi 
 |-  ( <. A , B >. .o. D ) = ( <. A , B >. ( comp ` C ) D )
42 3 10 12 14 16 17 22 27 39 40 41 rcaninv 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> ( ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) -> G = ( F ( <. B , A >. .o. D ) K ) ) )
43 7 9 42 sylc 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> G = ( F ( <. B , A >. .o. D ) K ) )