Metamath Proof Explorer

Theorem initoeu2lem2

Description: Lemma 2 for initoeu2 . (Contributed by AV, 10-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 initoeu2lem2 
|- ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) -> ( E! f f e. ( A H D ) -> E! g g e. ( B H D ) ) )

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 ovex 
 |-  ( F ( <. B , A >. .o. D ) K ) e. _V
8 eleq1 
 |-  ( g = ( F ( <. B , A >. .o. D ) K ) -> ( g e. ( B H D ) <-> ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) )
9 8 spcegv 
 |-  ( ( F ( <. B , A >. .o. D ) K ) e. _V -> ( ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) -> E. g g e. ( B H D ) ) )
10 7 9 mp1i 
 |-  ( ph -> ( ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) -> E. g g e. ( B H D ) ) )
11 10 com12 
 |-  ( ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) -> ( ph -> E. g g e. ( B H D ) ) )
12 11 3ad2ant3 
 |-  ( ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) -> ( ph -> E. g g e. ( B H D ) ) )
13 12 com12 
 |-  ( ph -> ( ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) -> E. g g e. ( B H D ) ) )
14 13 a1d 
 |-  ( ph -> ( ( A e. X /\ B e. X /\ D e. X ) -> ( ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) -> E. g g e. ( B H D ) ) ) )
15 14 3imp 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) -> E. g g e. ( B H D ) )
16 15 adantr 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) -> E. g g e. ( B H D ) )
17 simpll1 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ g e. ( B H D ) ) -> ph )
18 simpll2 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ g e. ( B H D ) ) -> ( A e. X /\ B e. X /\ D e. X ) )
19 3simpb 
 |-  ( ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) -> ( K e. ( B I A ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) )
20 19 3ad2ant3 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) -> ( K e. ( B I A ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) )
21 20 adantr 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) -> ( K e. ( B I A ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) )
22 21 adantr 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ g e. ( B H D ) ) -> ( K e. ( B I A ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) )
23 simplr 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ g e. ( B H D ) ) -> E! f f e. ( A H D ) )
24 simpl32 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) -> F e. ( A H D ) )
25 24 adantr 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ g e. ( B H D ) ) -> F e. ( A H D ) )
26 simpr 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ g e. ( B H D ) ) -> g e. ( B H D ) )
27 1 2 3 4 5 6 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 ) ) )
28 27 imp 
 |-  ( ( ( 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 ) )
29 17 18 22 23 25 26 28 syl33anc 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ g e. ( B H D ) ) -> g = ( F ( <. B , A >. .o. D ) K ) )
30 29 adantrr 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ ( g e. ( B H D ) /\ h e. ( B H D ) ) ) -> g = ( F ( <. B , A >. .o. D ) K ) )
31 simpll1 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ h e. ( B H D ) ) -> ph )
32 simpll2 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ h e. ( B H D ) ) -> ( A e. X /\ B e. X /\ D e. X ) )
33 21 adantr 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ h e. ( B H D ) ) -> ( K e. ( B I A ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) )
34 simplr 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ h e. ( B H D ) ) -> E! f f e. ( A H D ) )
35 24 adantr 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ h e. ( B H D ) ) -> F e. ( A H D ) )
36 simpr 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ h e. ( B H D ) ) -> h e. ( B H D ) )
37 1 2 3 4 5 6 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 ) /\ h e. ( B H D ) ) -> h = ( F ( <. B , A >. .o. D ) K ) ) )
38 37 imp 
 |-  ( ( ( 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 ) /\ h e. ( B H D ) ) ) -> h = ( F ( <. B , A >. .o. D ) K ) )
39 31 32 33 34 35 36 38 syl33anc 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ h e. ( B H D ) ) -> h = ( F ( <. B , A >. .o. D ) K ) )
40 39 adantrl 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ ( g e. ( B H D ) /\ h e. ( B H D ) ) ) -> h = ( F ( <. B , A >. .o. D ) K ) )
41 30 40 eqtr4d 
 |-  ( ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) /\ ( g e. ( B H D ) /\ h e. ( B H D ) ) ) -> g = h )
42 41 ex 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) -> ( ( g e. ( B H D ) /\ h e. ( B H D ) ) -> g = h ) )
43 42 alrimivv 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) -> A. g A. h ( ( g e. ( B H D ) /\ h e. ( B H D ) ) -> g = h ) )
44 eleq1 
 |-  ( g = h -> ( g e. ( B H D ) <-> h e. ( B H D ) ) )
45 44 eu4 
 |-  ( E! g g e. ( B H D ) <-> ( E. g g e. ( B H D ) /\ A. g A. h ( ( g e. ( B H D ) /\ h e. ( B H D ) ) -> g = h ) ) )
46 16 43 45 sylanbrc 
 |-  ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) /\ E! f f e. ( A H D ) ) -> E! g g e. ( B H D ) )
47 46 ex 
 |-  ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) -> ( E! f f e. ( A H D ) -> E! g g e. ( B H D ) ) )