initoeu2lem1

	Ref	Expression
Hypotheses	initoeu1.c	$⊢ φ \to C \in Cat$
	initoeu1.a	$⊢ φ \to A \in 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	initoeu2lem1	Could not format assertion : 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 \|-

Proof

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

Metamath Proof Explorer

Theorem initoeu2lem1

Proof