Theorem initoeu2lem2

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

	Ref	Expression
Hypotheses	initoeu1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	initoeu1.a	$$⊢\phi \to A\in \mathrm{InitO}\left(C\right)$$
	initoeu2lem.x	$$⊢X={\mathrm{Base}}_C$$
	initoeu2lem.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	initoeu2lem.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
	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	$$⊢\phi \to C\in \mathrm{Cat}$$
2		initoeu1.a	$$⊢\phi \to A\in \mathrm{InitO}\left(C\right)$$
3		initoeu2lem.x	$$⊢X={\mathrm{Base}}_C$$
4		initoeu2lem.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
5		initoeu2lem.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
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\to \left(g\in \left(BHD\right)\leftrightarrow h\in \left(BHD\right)\right)$$
45	44	eu4	$$⊢\exists !gg\in \left(BHD\right)\leftrightarrow \left(\exists gg\in \left(BHD\right)\wedge \forall g\forall h\left(\left(g\in \left(BHD\right)\wedge h\in \left(BHD\right)\right)\to g=h\right)\right)$$
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 |-