Metamath Proof Explorer

Theorem initoeu2lem1

Description: Lemma 1 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 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 ) ) )

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 eusn 
 |-  ( E! f f e. ( A H D ) <-> E. f ( A H D ) = { f } )
8 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
9 1 ad2antrr 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ K e. ( B I A ) ) -> C e. Cat )
10 simpr2 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) -> B e. X )
11 10 adantr 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ K e. ( B I A ) ) -> B e. X )
12 simpr1 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) -> A e. X )
13 12 adantr 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ K e. ( B I A ) ) -> A e. X )
14 3 8 9 11 13 5 invf 
 |-  ( ( ( 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 ) )
15 simpr 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ K e. ( B I A ) ) -> K e. ( B I A ) )
16 14 15 ffvelrnd 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ K e. ( B I A ) ) -> ( ( B ( Inv ` C ) A ) ` K ) e. ( A I B ) )
17 1 adantr 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) -> C e. Cat )
18 3 4 5 17 12 10 isohom 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) -> ( A I B ) C_ ( A H B ) )
19 18 adantr 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ K e. ( B I A ) ) -> ( A I B ) C_ ( A H B ) )
20 19 sselda 
 |-  ( ( ( ( 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 ) )
21 17 ad4antr 
 |-  ( ( ( ( ( ( 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 )
22 12 ad4antr 
 |-  ( ( ( ( ( ( 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 )
23 10 ad4antr 
 |-  ( ( ( ( ( ( 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 )
24 simpr3 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) -> D e. X )
25 24 ad4antr 
 |-  ( ( ( ( ( ( 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 )
26 simplr 
 |-  ( ( ( ( ( ( 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 ) )
27 simpr 
 |-  ( ( ( ( ( ( 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 ) )
28 3 4 6 21 22 23 25 26 27 catcocl 
 |-  ( ( ( ( ( ( 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 ) )
29 17 ad2antrr 
 |-  ( ( ( ( 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 )
30 12 ad2antrr 
 |-  ( ( ( ( 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 )
31 10 ad2antrr 
 |-  ( ( ( ( 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 )
32 24 ad2antrr 
 |-  ( ( ( ( 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 )
33 simplr 
 |-  ( ( ( ( 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 ) )
34 simpr 
 |-  ( ( ( ( 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 ) )
35 3 4 6 29 30 31 32 33 34 catcocl 
 |-  ( ( ( ( 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 ) )
36 35 exp31 
 |-  ( ( 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 ) ) ) )
37 36 ad2antrr 
 |-  ( ( ( ( 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 37 imp 
 |-  ( ( ( ( ( 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 ) ) )
39 eleq2 
 |-  ( ( 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 39 adantl 
 |-  ( ( ( ( ( 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 } ) )
41 ovex 
 |-  ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) e. _V
42 elsng 
 |-  ( ( ( 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 ) )
43 41 42 mp1i 
 |-  ( ( ( ( ( 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 ) )
44 40 43 bitrd 
 |-  ( ( ( ( ( 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 ) )
45 eleq2 
 |-  ( ( 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 } ) )
46 ovex 
 |-  ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) e. _V
47 elsng 
 |-  ( ( 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 ) )
48 46 47 mp1i 
 |-  ( ( 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 ) )
49 45 48 bitrd 
 |-  ( ( 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 49 adantl 
 |-  ( ( ( ( ( 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 ) )
51 eqeq2 
 |-  ( 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 ) ) ) )
52 51 eqcoms 
 |-  ( ( 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 52 adantl 
 |-  ( ( ( ( ( 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 ) ) ) )
54 simp-4l 
 |-  ( ( ( ( ( ( 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 ) ) )
55 simp-4r 
 |-  ( ( ( ( ( ( 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 ) )
56 simprr 
 |-  ( ( ( ( ( ( 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 ) )
57 simprl 
 |-  ( ( ( ( ( ( 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 ) )
58 simplr 
 |-  ( ( ( ( ( ( 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 ) ) )
59 1 2 3 4 5 6 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 ) )
60 54 55 56 57 58 59 syl131anc 
 |-  ( ( ( ( ( ( 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 ) )
61 60 exp43 
 |-  ( ( ( ( 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 ) ) ) ) )
62 61 adantr 
 |-  ( ( ( ( ( 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 ) ) ) ) )
63 53 62 sylbid 
 |-  ( ( ( ( ( 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 ) ) ) ) )
64 63 ex 
 |-  ( ( ( ( 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 ) ) ) ) ) )
65 64 adantr 
 |-  ( ( ( ( ( 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 ) ) ) ) ) )
66 50 65 sylbid 
 |-  ( ( ( ( ( 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 ) ) ) ) ) )
67 66 com23 
 |-  ( ( ( ( ( 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 ) ) ) ) ) )
68 44 67 sylbid 
 |-  ( ( ( ( ( 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 ) ) ) ) ) )
69 68 com23 
 |-  ( ( ( ( ( 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 ) ) ) ) ) )
70 69 ex 
 |-  ( ( ( ( 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 ) ) ) ) ) ) )
71 70 com24 
 |-  ( ( ( ( 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 ) ) ) ) ) ) )
72 71 adantr 
 |-  ( ( ( ( ( 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 ) ) ) ) ) ) )
73 38 72 syld 
 |-  ( ( ( ( ( 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 ) ) ) ) ) ) )
74 73 com25 
 |-  ( ( ( ( ( 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 ) ) ) ) ) ) )
75 74 imp 
 |-  ( ( ( ( ( ( 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 ) ) ) ) ) )
76 28 75 mpd 
 |-  ( ( ( ( ( ( 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 ) ) ) ) )
77 76 ex 
 |-  ( ( ( ( ( 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 ) ) ) ) ) )
78 20 77 mpdan 
 |-  ( ( ( ( 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 ) ) ) ) ) )
79 78 com15 
 |-  ( 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 ) ) ) ) ) )
80 79 imp 
 |-  ( ( 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 ) ) ) ) )
81 80 impcom 
 |-  ( ( ( 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 ) ) ) )
82 81 com13 
 |-  ( ( ( ( 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 ) ) ) )
83 16 82 mpdan 
 |-  ( ( ( 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 ) ) ) )
84 83 expimpd 
 |-  ( ( 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 ) ) ) )
85 84 3impia 
 |-  ( ( 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 ) ) )
86 85 com12 
 |-  ( ( ( 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 ) ) )
87 86 ex 
 |-  ( ( 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 ) ) ) )
88 87 exlimiv 
 |-  ( 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 ) ) ) )
89 7 88 sylbi 
 |-  ( 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 ) ) ) )
90 89 3impib 
 |-  ( ( 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 ) ) )
91 90 com12 
 |-  ( ( 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 ) ) )