MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  initoeu2lem1 Structured version   Visualization version   Unicode version

Theorem initoeu2lem1 15964
Description: Lemma 1 for initoeu2 15966. (Contributed by AV, 9-Apr-2020.)
Hypotheses
Ref Expression
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
Ref Expression
initoeu2lem1  |-  ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )  /\  ( K  e.  ( B I A )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) ) )  ->  (
( E! f  f  e.  ( A H D )  /\  F  e.  ( A H D )  /\  G  e.  ( B H D ) )  ->  G  =  ( F (
<. B ,  A >.  .o. 
D ) K ) ) )
Distinct variable groups:    A, f    B, f    C, f    ph, f    D, f    f, F    f, G    f, I    f, K   
f, H    f, X    .o. , f

Proof of Theorem initoeu2lem1
StepHypRef Expression
1 eusn 4061 . . . 4  |-  ( E! f  f  e.  ( A H D )  <->  E. f ( A H D )  =  {
f } )
2 initoeu2lem.x . . . . . . . . . . . 12  |-  X  =  ( Base `  C
)
3 eqid 2462 . . . . . . . . . . . 12  |-  (Inv `  C )  =  (Inv
`  C )
4 initoeu1.c . . . . . . . . . . . . 13  |-  ( ph  ->  C  e.  Cat )
54ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )
)  /\  K  e.  ( B I A ) )  ->  C  e.  Cat )
6 simpr2 1021 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  ->  B  e.  X )
76adantr 471 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )
)  /\  K  e.  ( B I A ) )  ->  B  e.  X )
8 simpr1 1020 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  ->  A  e.  X )
98adantr 471 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )
)  /\  K  e.  ( B I A ) )  ->  A  e.  X )
10 initoeu2lem.i . . . . . . . . . . . 12  |-  I  =  (  Iso  `  C
)
112, 3, 5, 7, 9, 10invf 15728 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )
)  /\  K  e.  ( B I A ) )  ->  ( B
(Inv `  C ) A ) : ( B I A ) --> ( A I B ) )
12 simpr 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )
)  /\  K  e.  ( B I A ) )  ->  K  e.  ( B I A ) )
1311, 12ffvelrnd 6051 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )
)  /\  K  e.  ( B I A ) )  ->  ( ( B (Inv `  C ) A ) `  K
)  e.  ( A I B ) )
14 initoeu2lem.h . . . . . . . . . . . . . . . . . 18  |-  H  =  ( Hom  `  C
)
154adantr 471 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  ->  C  e.  Cat )
162, 14, 10, 15, 8, 6isohom 15736 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  -> 
( A I B )  C_  ( A H B ) )
1716adantr 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )
)  /\  K  e.  ( B I A ) )  ->  ( A I B )  C_  ( A H B ) )
1817sselda 3444 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  ->  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )
19 initoeu2lem.o . . . . . . . . . . . . . . . . . 18  |-  .o.  =  (comp `  C )
2015ad4antr 743 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A H B ) )  /\  G  e.  ( B H D ) )  ->  C  e.  Cat )
218ad4antr 743 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A H B ) )  /\  G  e.  ( B H D ) )  ->  A  e.  X )
226ad4antr 743 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A H B ) )  /\  G  e.  ( B H D ) )  ->  B  e.  X )
23 simpr3 1022 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  ->  D  e.  X )
2423ad4antr 743 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A H B ) )  /\  G  e.  ( B H D ) )  ->  D  e.  X )
25 simplr 767 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A H B ) )  /\  G  e.  ( B H D ) )  -> 
( ( B (Inv
`  C ) A ) `  K )  e.  ( A H B ) )
26 simpr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A H B ) )  /\  G  e.  ( B H D ) )  ->  G  e.  ( B H D ) )
272, 14, 19, 20, 21, 22, 24, 25, 26catcocl 15646 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A H B ) )  /\  G  e.  ( B H D ) )  -> 
( G ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e.  ( A H D ) )
2815ad2antrr 737 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) )  ->  C  e.  Cat )
298ad2antrr 737 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) )  ->  A  e.  X )
306ad2antrr 737 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) )  ->  B  e.  X )
3123ad2antrr 737 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) )  ->  D  e.  X )
32 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) )  ->  ( ( B (Inv `  C ) A ) `  K
)  e.  ( A H B ) )
33 simpr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) )  ->  ( F
( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) )
342, 14, 19, 28, 29, 30, 31, 32, 33catcocl 15646 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) )  ->  ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e.  ( A H D ) )
3534exp31 613 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  -> 
( ( ( B (Inv `  C ) A ) `  K
)  e.  ( A H B )  -> 
( ( F (
<. B ,  A >.  .o. 
D ) K )  e.  ( B H D )  ->  (
( F ( <. B ,  A >.  .o. 
D ) K ) ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  ( A H D ) ) ) )
3635ad2antrr 737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  ->  (
( ( B (Inv
`  C ) A ) `  K )  e.  ( A H B )  ->  (
( F ( <. B ,  A >.  .o. 
D ) K )  e.  ( B H D )  ->  (
( F ( <. B ,  A >.  .o. 
D ) K ) ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  ( A H D ) ) ) )
3736imp 435 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )  ->  (
( F ( <. B ,  A >.  .o. 
D ) K )  e.  ( B H D )  ->  (
( F ( <. B ,  A >.  .o. 
D ) K ) ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  ( A H D ) ) )
38 eleq2 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( A H D )  =  { f }  ->  ( ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e.  ( A H D )  <->  ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  e.  { f } ) )
3938adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  ( A H D )  =  { f } )  ->  ( ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e.  ( A H D )  <->  ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  e.  { f } ) )
40 ovex 6348 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e. 
_V
41 elsncg 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( F ( <. B ,  A >.  .o. 
D ) K ) ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  _V  ->  (
( ( F (
<. B ,  A >.  .o. 
D ) K ) ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  { f }  <-> 
( ( F (
<. B ,  A >.  .o. 
D ) K ) ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  =  f ) )
4240, 41mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  ( A H D )  =  { f } )  ->  ( ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e. 
{ f }  <->  ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  =  f ) )
4339, 42bitrd 261 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  ( A H D )  =  { f } )  ->  ( ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e.  ( A H D )  <->  ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  =  f ) )
44 eleq2 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A H D )  =  { f }  ->  ( ( G ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  ( A H D )  <->  ( G
( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  { f } ) )
45 ovex 6348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( G ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  _V
46 elsncg 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( G ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  e.  _V  ->  ( ( G ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e. 
{ f }  <->  ( G
( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  =  f ) )
4745, 46mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A H D )  =  { f }  ->  ( ( G ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  { f }  <-> 
( G ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  =  f ) )
4844, 47bitrd 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( A H D )  =  { f }  ->  ( ( G ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  ( A H D )  <->  ( G
( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  =  f ) )
4948adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  ( A H D )  =  { f } )  ->  ( ( G ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  ( A H D )  <->  ( G
( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  =  f ) )
50 eqeq2 2473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f  =  ( 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 ) )  =  f  <->  ( ( 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 ) ) ) )
5150eqcoms 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( G ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  =  f  -> 
( ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  =  f  <->  ( ( 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 ) ) ) )
5251adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  ( G ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  =  f )  ->  ( ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  =  f  <->  ( ( 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 ) ) ) )
53 simp-4l 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( 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  e.  ( B H D )  /\  F  e.  ( A H D ) ) )  -> 
( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )
) )
54 simp-4r 782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( 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  e.  ( B H D )  /\  F  e.  ( A H D ) ) )  ->  K  e.  ( B I A ) )
55 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( 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  e.  ( B H D )  /\  F  e.  ( A H D ) ) )  ->  F  e.  ( A H D ) )
56 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( 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  e.  ( B H D )  /\  F  e.  ( A H D ) ) )  ->  G  e.  ( B H D ) )
57 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( 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  e.  ( B H D )  /\  F  e.  ( A 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 ) ) )
58 initoeu1.a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  A  e.  (InitO `  C ) )
594, 58, 2, 14, 10, 19initoeu2lem0 15963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( 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 ) )
6053, 54, 55, 56, 57, 59syl131anc 1289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( 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  e.  ( B H D )  /\  F  e.  ( A H D ) ) )  ->  G  =  ( F
( <. B ,  A >.  .o.  D ) K ) )
6160exp43 621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  ->  (
( ( 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  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) ) )
6261adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  ( G ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  =  f )  ->  ( ( ( 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  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) ) )
6352, 62sylbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  ( G ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  =  f )  ->  ( ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  =  f  ->  ( G  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) ) )
6463ex 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  ->  (
( G ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  =  f  ->  ( (
( F ( <. B ,  A >.  .o. 
D ) K ) ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  =  f  ->  ( G  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F (
<. B ,  A >.  .o. 
D ) K ) ) ) ) ) )
6564adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  ( A H D )  =  { f } )  ->  ( ( G ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  =  f  ->  (
( ( F (
<. B ,  A >.  .o. 
D ) K ) ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  =  f  ->  ( G  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F (
<. B ,  A >.  .o. 
D ) K ) ) ) ) ) )
6649, 65sylbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  ( A H D )  =  { f } )  ->  ( ( G ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  ( A H D )  ->  (
( ( F (
<. B ,  A >.  .o. 
D ) K ) ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  =  f  ->  ( G  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F (
<. B ,  A >.  .o. 
D ) K ) ) ) ) ) )
6766com23 81 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  ( A H D )  =  { f } )  ->  ( ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  =  f  ->  ( ( G ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  e.  ( A H D )  -> 
( G  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) ) ) )
6843, 67sylbid 223 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  ( A H D )  =  { f } )  ->  ( ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e.  ( A H D )  ->  ( ( G ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  e.  ( A H D )  -> 
( G  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) ) ) )
6968com23 81 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  ( A H D )  =  { f } )  ->  ( ( G ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  ( A H D )  ->  (
( ( F (
<. B ,  A >.  .o. 
D ) K ) ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  ( A H D )  ->  ( G  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F (
<. B ,  A >.  .o. 
D ) K ) ) ) ) ) )
7069ex 440 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  ->  (
( A H D )  =  { f }  ->  ( ( G ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  e.  ( A H D )  -> 
( ( ( F ( <. B ,  A >.  .o.  D ) K ) ( <. A ,  B >.  .o.  D )
( ( B (Inv
`  C ) A ) `  K ) )  e.  ( A H D )  -> 
( G  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) ) ) ) )
7170com24 90 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  ->  (
( ( F (
<. B ,  A >.  .o. 
D ) K ) ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  ( A H D )  ->  (
( G ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e.  ( A H D )  ->  ( ( A H D )  =  { f }  ->  ( G  e.  ( B H D )  -> 
( F  e.  ( A H D )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) ) ) ) )
7271adantr 471 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )  ->  (
( ( F (
<. B ,  A >.  .o. 
D ) K ) ( <. A ,  B >.  .o.  D ) ( ( B (Inv `  C ) A ) `
 K ) )  e.  ( A H D )  ->  (
( G ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e.  ( A H D )  ->  ( ( A H D )  =  { f }  ->  ( G  e.  ( B H D )  -> 
( F  e.  ( A H D )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) ) ) ) )
7337, 72syld 45 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )  ->  (
( F ( <. B ,  A >.  .o. 
D ) K )  e.  ( B H D )  ->  (
( G ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e.  ( A H D )  ->  ( ( A H D )  =  { f }  ->  ( G  e.  ( B H D )  -> 
( F  e.  ( A H D )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) ) ) ) )
7473com25 94 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )  ->  ( G  e.  ( B H D )  ->  (
( G ( <. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e.  ( A H D )  ->  ( ( A H D )  =  { f }  ->  ( ( F ( <. B ,  A >.  .o. 
D ) K )  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F (
<. B ,  A >.  .o. 
D ) K ) ) ) ) ) ) )
7574imp 435 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A H B ) )  /\  G  e.  ( B H D ) )  -> 
( ( G (
<. A ,  B >.  .o. 
D ) ( ( B (Inv `  C
) A ) `  K ) )  e.  ( A H D )  ->  ( ( A H D )  =  { f }  ->  ( ( F ( <. B ,  A >.  .o. 
D ) K )  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F (
<. B ,  A >.  .o. 
D ) K ) ) ) ) ) )
7627, 75mpd 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A I B ) )  /\  ( ( B (Inv
`  C ) A ) `  K )  e.  ( A H B ) )  /\  G  e.  ( B H D ) )  -> 
( ( A H D )  =  {
f }  ->  (
( F ( <. B ,  A >.  .o. 
D ) K )  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F (
<. B ,  A >.  .o. 
D ) K ) ) ) ) )
7776ex 440 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A H B ) )  ->  ( G  e.  ( B H D )  ->  (
( A H D )  =  { f }  ->  ( ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) ) ) )
7818, 77mpdan 679 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  ->  ( G  e.  ( B H D )  ->  (
( A H D )  =  { f }  ->  ( ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D )  ->  ( F  e.  ( A H D )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) ) ) )
7978com15 96 . . . . . . . . . . . . 13  |-  ( F  e.  ( A H D )  ->  ( G  e.  ( B H D )  ->  (
( A H D )  =  { f }  ->  ( ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D )  ->  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )
)  /\  K  e.  ( B I A ) )  /\  ( ( B (Inv `  C
) A ) `  K )  e.  ( A I B ) )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) ) ) )
8079imp 435 . . . . . . . . . . . 12  |-  ( ( F  e.  ( A H D )  /\  G  e.  ( B H D ) )  -> 
( ( A H D )  =  {
f }  ->  (
( F ( <. B ,  A >.  .o. 
D ) K )  e.  ( B H D )  ->  (
( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  ->  G  =  ( F (
<. B ,  A >.  .o. 
D ) K ) ) ) ) )
8180impcom 436 . . . . . . . . . . 11  |-  ( ( ( A H D )  =  { f }  /\  ( F  e.  ( A H D )  /\  G  e.  ( B H D ) ) )  -> 
( ( F (
<. B ,  A >.  .o. 
D ) K )  e.  ( B H D )  ->  (
( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  ->  G  =  ( F (
<. B ,  A >.  .o. 
D ) K ) ) ) )
8281com13 83 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
) )  /\  K  e.  ( B I A ) )  /\  (
( B (Inv `  C ) A ) `
 K )  e.  ( A I B ) )  ->  (
( F ( <. B ,  A >.  .o. 
D ) K )  e.  ( B H D )  ->  (
( ( A H D )  =  {
f }  /\  ( F  e.  ( A H D )  /\  G  e.  ( B H D ) ) )  ->  G  =  ( F
( <. B ,  A >.  .o.  D ) K ) ) ) )
8313, 82mpdan 679 . . . . . . . . 9  |-  ( ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )
)  /\  K  e.  ( B I A ) )  ->  ( ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D )  ->  ( ( ( A H D )  =  { f }  /\  ( F  e.  ( A H D )  /\  G  e.  ( B H D ) ) )  ->  G  =  ( F
( <. B ,  A >.  .o.  D ) K ) ) ) )
8483expimpd 612 . . . . . . . 8  |-  ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X ) )  -> 
( ( K  e.  ( B I A )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) )  ->  ( ( ( A H D )  =  { f }  /\  ( F  e.  ( A H D )  /\  G  e.  ( B H D ) ) )  ->  G  =  ( F
( <. B ,  A >.  .o.  D ) K ) ) ) )
85843impia 1212 . . . . . . 7  |-  ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )  /\  ( K  e.  ( B I A )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) ) )  ->  (
( ( A H D )  =  {
f }  /\  ( F  e.  ( A H D )  /\  G  e.  ( B H D ) ) )  ->  G  =  ( F
( <. B ,  A >.  .o.  D ) K ) ) )
8685com12 32 . . . . . 6  |-  ( ( ( A H D )  =  { f }  /\  ( F  e.  ( A H D )  /\  G  e.  ( B H D ) ) )  -> 
( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X
)  /\  ( K  e.  ( B I A )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) ) )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) )
8786ex 440 . . . . 5  |-  ( ( A H D )  =  { f }  ->  ( ( F  e.  ( A H D )  /\  G  e.  ( B H D ) )  ->  (
( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )  /\  ( K  e.  ( B I A )  /\  ( F (
<. B ,  A >.  .o. 
D ) K )  e.  ( B H D ) ) )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) )
8887exlimiv 1787 . . . 4  |-  ( E. f ( A H D )  =  {
f }  ->  (
( F  e.  ( A H D )  /\  G  e.  ( B H D ) )  ->  ( ( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )  /\  ( K  e.  ( B I A )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) ) )  ->  G  =  ( F (
<. B ,  A >.  .o. 
D ) K ) ) ) )
891, 88sylbi 200 . . 3  |-  ( E! f  f  e.  ( A H D )  ->  ( ( F  e.  ( A H D )  /\  G  e.  ( B H D ) )  ->  (
( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )  /\  ( K  e.  ( B I A )  /\  ( F (
<. B ,  A >.  .o. 
D ) K )  e.  ( B H D ) ) )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) ) )
90893impib 1213 . 2  |-  ( ( E! f  f  e.  ( A H D )  /\  F  e.  ( A H D )  /\  G  e.  ( B H D ) )  ->  (
( ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )  /\  ( K  e.  ( B I A )  /\  ( F (
<. B ,  A >.  .o. 
D ) K )  e.  ( B H D ) ) )  ->  G  =  ( F ( <. B ,  A >.  .o.  D ) K ) ) )
9190com12 32 1  |-  ( (
ph  /\  ( A  e.  X  /\  B  e.  X  /\  D  e.  X )  /\  ( K  e.  ( B I A )  /\  ( F ( <. B ,  A >.  .o.  D ) K )  e.  ( B H D ) ) )  ->  (
( E! f  f  e.  ( A H D )  /\  F  e.  ( A H D )  /\  G  e.  ( B H D ) )  ->  G  =  ( F (
<. B ,  A >.  .o. 
D ) K ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455   E.wex 1674    e. wcel 1898   E!weu 2310   _Vcvv 3057    C_ wss 3416   {csn 3980   <.cop 3986   ` cfv 5605  (class class class)co 6320   Basecbs 15176   Hom chom 15256  compcco 15257   Catccat 15625  Invcinv 15705    Iso ciso 15706  InitOcinito 15938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-1st 6825  df-2nd 6826  df-cat 15629  df-cid 15630  df-sect 15707  df-inv 15708  df-iso 15709
This theorem is referenced by:  initoeu2lem2  15965
  Copyright terms: Public domain W3C validator