Metamath Proof Explorer

Theorem initoeu2lem1

Description: Lemma 1 for initoeu2 . (Contributed by AV, 9-Apr-2020)

Ref Expression
Hypotheses initoeu1.c ⊢φ→C∈Cat
initoeu1.a ⊢φ→A∈InitO⁡C
initoeu2lem.x ⊢X=BaseC
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 ⊢φ→C∈Cat
2 initoeu1.a ⊢φ→A∈InitO⁡C
3 initoeu2lem.x ⊢X=BaseC
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 ⊢∃!ff∈AHD↔∃fAHD=f
8 eqid ⊢Inv⁡C=Inv⁡C
9 1 ad2antrr ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA→C∈Cat
10 simpr2 ⊢φ∧A∈X∧B∈X∧D∈X→B∈X
11 10 adantr ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA→B∈X
12 simpr1 ⊢φ∧A∈X∧B∈X∧D∈X→A∈X
13 12 adantr ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA→A∈X
14 3 8 9 11 13 5 invf ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA→BInv⁡CA:BIA⟶AIB
15 simpr ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA→K∈BIA
16 14 15 ffvelcdmd ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA→BInv⁡CA⁡K∈AIB
17 1 adantr ⊢φ∧A∈X∧B∈X∧D∈X→C∈Cat
18 3 4 5 17 12 10 isohom ⊢φ∧A∈X∧B∈X∧D∈X→AIB⊆AHB
19 18 adantr ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA→AIB⊆AHB
20 19 sselda ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA∧BInv⁡CA⁡K∈AIB→BInv⁡CA⁡K∈AHB
21 17 ad4antr ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA∧BInv⁡CA⁡K∈AIB∧BInv⁡CA⁡K∈AHB∧G∈BHD→C∈Cat
22 12 ad4antr ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA∧BInv⁡CA⁡K∈AIB∧BInv⁡CA⁡K∈AHB∧G∈BHD→A∈X
23 10 ad4antr ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA∧BInv⁡CA⁡K∈AIB∧BInv⁡CA⁡K∈AHB∧G∈BHD→B∈X
24 simpr3 ⊢φ∧A∈X∧B∈X∧D∈X→D∈X
25 24 ad4antr ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA∧BInv⁡CA⁡K∈AIB∧BInv⁡CA⁡K∈AHB∧G∈BHD→D∈X
26 simplr ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA∧BInv⁡CA⁡K∈AIB∧BInv⁡CA⁡K∈AHB∧G∈BHD→BInv⁡CA⁡K∈AHB
27 simpr ⊢φ∧A∈X∧B∈X∧D∈X∧K∈BIA∧BInv⁡CA⁡K∈AIB∧BInv⁡CA⁡K∈AHB∧G∈BHD→G∈BHD
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 |-