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

Metamath Proof Explorer

Theorem initoeu2lem2

Description: Lemma 2 for initoeu2 . (Contributed by AV, 10-Apr-2020)

Ref Expression
Hypotheses initoeu1.c ⊢ φ → C ∈ Cat
initoeu1.a ⊢ φ → A ∈ InitO ⁡ C
initoeu2lem.x ⊢ X = Base C
initoeu2lem.h ⊢ H = Hom ⁡ C
initoeu2lem.i ⊢ I = Iso ⁡ C
initoeu2lem.o No typesetting found for |- .o. = ( comp ` C ) with typecode |-
Assertion initoeu2lem2 Could not format assertion : No typesetting found for |- ( ( 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 ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 initoeu1.c ⊢ φ → C ∈ Cat
2 initoeu1.a ⊢ φ → A ∈ InitO ⁡ C
3 initoeu2lem.x ⊢ X = Base C
4 initoeu2lem.h ⊢ H = Hom ⁡ C
5 initoeu2lem.i ⊢ I = Iso ⁡ C
6 initoeu2lem.o Could not format .o. = ( comp ` C ) : No typesetting found for |- .o. = ( comp ` C ) with typecode |-
7 ovex Could not format ( F ( <. B , A >. .o. D ) K ) e. _V : No typesetting found for |- ( F ( <. B , A >. .o. D ) K ) e. _V with typecode |-
8 eleq1 Could not format ( g = ( F ( <. B , A >. .o. D ) K ) -> ( g e. ( B H D ) <-> ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) : No typesetting found for |- ( g = ( F ( <. B , A >. .o. D ) K ) -> ( g e. ( B H D ) <-> ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) ) ) with typecode |-
9 8 spcegv Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
10 7 9 mp1i Could not format ( ph -> ( ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) -> E. g g e. ( B H D ) ) ) : No typesetting found for |- ( ph -> ( ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) -> E. g g e. ( B H D ) ) ) with typecode |-
11 10 com12 Could not format ( ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) -> ( ph -> E. g g e. ( B H D ) ) ) : No typesetting found for |- ( ( F ( <. B , A >. .o. D ) K ) e. ( B H D ) -> ( ph -> E. g g e. ( B H D ) ) ) with typecode |-
12 11 3ad2ant3 Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
13 12 com12 Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
14 13 a1d Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
15 14 3imp Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
16 15 adantr Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
17 simpll1 Could not format ( ( ( ( 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 ) : No typesetting found for |- ( ( ( ( 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 ) with typecode |-
18 simpll2 Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
19 3simpb Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
20 19 3ad2ant3 Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
21 20 adantr Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-
22 21 adantr Could not format ( ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( ( 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 ) ) ) with typecode |-
23 simplr Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
24 simpl32 Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
25 24 adantr Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
26 simpr Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
27 1 2 3 4 5 6 initoeu2lem1 Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
28 27 imp Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
29 17 18 22 23 25 26 28 syl33anc Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
30 29 adantrr Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
31 simpll1 Could not format ( ( ( ( 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 ) : No typesetting found for |- ( ( ( ( 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 ) with typecode |-
32 simpll2 Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
33 21 adantr Could not format ( ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( ( 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 ) ) ) with typecode |-
34 simplr Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
35 24 adantr Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
36 simpr Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
37 1 2 3 4 5 6 initoeu2lem1 Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
38 37 imp Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
39 31 32 33 34 35 36 38 syl33anc Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
40 39 adantrl Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
41 30 40 eqtr4d Could not format ( ( ( ( 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 ) : No typesetting found for |- ( ( ( ( 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 ) with typecode |-
42 41 ex Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
43 42 alrimivv Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
44 eleq1 ⊢ g = h → g ∈ B H D ↔ h ∈ B H D
45 44 eu4 ⊢ ∃! g g ∈ B H D ↔ ∃ g g ∈ B H D ∧ ∀ g ∀ h g ∈ B H D ∧ h ∈ B H D → g = h
46 16 43 45 sylanbrc Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
47 46 ex Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-