Metamath Proof Explorer


Theorem dfmgc2

Description: Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024)

Ref Expression
Hypotheses mgcoval.1 A=BaseV
mgcoval.2 B=BaseW
mgcoval.3 ˙=V
mgcoval.4 No typesetting found for |- .c_ = ( le ` W ) with typecode |-
mgcval.1 No typesetting found for |- H = ( V MGalConn W ) with typecode |-
mgcval.2 φVProset
mgcval.3 φWProset
Assertion dfmgc2 Could not format assertion : No typesetting found for |- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 mgcoval.1 A=BaseV
2 mgcoval.2 B=BaseW
3 mgcoval.3 ˙=V
4 mgcoval.4 Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5 mgcval.1 Could not format H = ( V MGalConn W ) : No typesetting found for |- H = ( V MGalConn W ) with typecode |-
6 mgcval.2 φVProset
7 mgcval.3 φWProset
8 1 2 3 4 5 6 7 mgcval Could not format ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) ) : No typesetting found for |- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) ) with typecode |-
9 8 simprbda φFHGF:ABG:BA
10 6 ad4antr φFHGxAyAx˙yVProset
11 7 ad4antr φFHGxAyAx˙yWProset
12 simp-4r φFHGxAyAx˙yFHG
13 simpllr φFHGxAyAx˙yxA
14 simplr φFHGxAyAx˙yyA
15 simpr φFHGxAyAx˙yx˙y
16 1 2 3 4 5 10 11 12 13 14 15 mgcmnt1 Could not format ( ( ( ( ( ph /\ F H G ) /\ x e. A ) /\ y e. A ) /\ x .<_ y ) -> ( F ` x ) .c_ ( F ` y ) ) : No typesetting found for |- ( ( ( ( ( ph /\ F H G ) /\ x e. A ) /\ y e. A ) /\ x .<_ y ) -> ( F ` x ) .c_ ( F ` y ) ) with typecode |-
17 16 ex Could not format ( ( ( ( ph /\ F H G ) /\ x e. A ) /\ y e. A ) -> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( ph /\ F H G ) /\ x e. A ) /\ y e. A ) -> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) with typecode |-
18 17 anasss Could not format ( ( ( ph /\ F H G ) /\ ( x e. A /\ y e. A ) ) -> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for |- ( ( ( ph /\ F H G ) /\ ( x e. A /\ y e. A ) ) -> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) with typecode |-
19 18 ralrimivva Could not format ( ( ph /\ F H G ) -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for |- ( ( ph /\ F H G ) -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) with typecode |-
20 6 ad4antr Could not format ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> V e. Proset ) : No typesetting found for |- ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> V e. Proset ) with typecode |-
21 7 ad4antr Could not format ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> W e. Proset ) : No typesetting found for |- ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> W e. Proset ) with typecode |-
22 simp-4r Could not format ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> F H G ) : No typesetting found for |- ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> F H G ) with typecode |-
23 simpllr Could not format ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> u e. B ) : No typesetting found for |- ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> u e. B ) with typecode |-
24 simplr Could not format ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> v e. B ) : No typesetting found for |- ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> v e. B ) with typecode |-
25 simpr Could not format ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> u .c_ v ) : No typesetting found for |- ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> u .c_ v ) with typecode |-
26 1 2 3 4 5 20 21 22 23 24 25 mgcmnt2 Could not format ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> ( G ` u ) .<_ ( G ` v ) ) : No typesetting found for |- ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> ( G ` u ) .<_ ( G ` v ) ) with typecode |-
27 26 ex Could not format ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) -> ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) : No typesetting found for |- ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) -> ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) with typecode |-
28 27 anasss Could not format ( ( ( ph /\ F H G ) /\ ( u e. B /\ v e. B ) ) -> ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) : No typesetting found for |- ( ( ( ph /\ F H G ) /\ ( u e. B /\ v e. B ) ) -> ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) with typecode |-
29 28 ralrimivva Could not format ( ( ph /\ F H G ) -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) : No typesetting found for |- ( ( ph /\ F H G ) -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) with typecode |-
30 19 29 jca Could not format ( ( ph /\ F H G ) -> ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) : No typesetting found for |- ( ( ph /\ F H G ) -> ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) with typecode |-
31 6 ad2antrr φFHGuBVProset
32 7 ad2antrr φFHGuBWProset
33 simplr φFHGuBFHG
34 simpr φFHGuBuB
35 1 2 3 4 5 31 32 33 34 mgccole2 Could not format ( ( ( ph /\ F H G ) /\ u e. B ) -> ( F ` ( G ` u ) ) .c_ u ) : No typesetting found for |- ( ( ( ph /\ F H G ) /\ u e. B ) -> ( F ` ( G ` u ) ) .c_ u ) with typecode |-
36 35 ralrimiva Could not format ( ( ph /\ F H G ) -> A. u e. B ( F ` ( G ` u ) ) .c_ u ) : No typesetting found for |- ( ( ph /\ F H G ) -> A. u e. B ( F ` ( G ` u ) ) .c_ u ) with typecode |-
37 6 ad2antrr φFHGxAVProset
38 7 ad2antrr φFHGxAWProset
39 simplr φFHGxAFHG
40 simpr φFHGxAxA
41 1 2 3 4 5 37 38 39 40 mgccole1 φFHGxAx˙GFx
42 41 ralrimiva φFHGxAx˙GFx
43 36 42 jca Could not format ( ( ph /\ F H G ) -> ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) : No typesetting found for |- ( ( ph /\ F H G ) -> ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) with typecode |-
44 30 43 jca Could not format ( ( ph /\ F H G ) -> ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) : No typesetting found for |- ( ( ph /\ F H G ) -> ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) with typecode |-
45 9 44 jca Could not format ( ( ph /\ F H G ) -> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) : No typesetting found for |- ( ( ph /\ F H G ) -> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) with typecode |-
46 6 ad4antr Could not format ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> V e. Proset ) : No typesetting found for |- ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> V e. Proset ) with typecode |-
47 7 ad4antr Could not format ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> W e. Proset ) : No typesetting found for |- ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> W e. Proset ) with typecode |-
48 simp-4r Could not format ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> ( F : A --> B /\ G : B --> A ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> ( F : A --> B /\ G : B --> A ) ) with typecode |-
49 48 simpld Could not format ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> F : A --> B ) : No typesetting found for |- ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> F : A --> B ) with typecode |-
50 48 simprd Could not format ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> G : B --> A ) : No typesetting found for |- ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> G : B --> A ) with typecode |-
51 simpllr Could not format ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) with typecode |-
52 51 simpld Could not format ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) with typecode |-
53 breq1 x=mx˙ym˙y
54 fveq2 x=mFx=Fm
55 54 breq1d Could not format ( x = m -> ( ( F ` x ) .c_ ( F ` y ) <-> ( F ` m ) .c_ ( F ` y ) ) ) : No typesetting found for |- ( x = m -> ( ( F ` x ) .c_ ( F ` y ) <-> ( F ` m ) .c_ ( F ` y ) ) ) with typecode |-
56 53 55 imbi12d Could not format ( x = m -> ( ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) <-> ( m .<_ y -> ( F ` m ) .c_ ( F ` y ) ) ) ) : No typesetting found for |- ( x = m -> ( ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) <-> ( m .<_ y -> ( F ` m ) .c_ ( F ` y ) ) ) ) with typecode |-
57 breq2 y=nm˙ym˙n
58 fveq2 y=nFy=Fn
59 58 breq2d Could not format ( y = n -> ( ( F ` m ) .c_ ( F ` y ) <-> ( F ` m ) .c_ ( F ` n ) ) ) : No typesetting found for |- ( y = n -> ( ( F ` m ) .c_ ( F ` y ) <-> ( F ` m ) .c_ ( F ` n ) ) ) with typecode |-
60 57 59 imbi12d Could not format ( y = n -> ( ( m .<_ y -> ( F ` m ) .c_ ( F ` y ) ) <-> ( m .<_ n -> ( F ` m ) .c_ ( F ` n ) ) ) ) : No typesetting found for |- ( y = n -> ( ( m .<_ y -> ( F ` m ) .c_ ( F ` y ) ) <-> ( m .<_ n -> ( F ` m ) .c_ ( F ` n ) ) ) ) with typecode |-
61 56 60 cbvral2vw Could not format ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) <-> A. m e. A A. n e. A ( m .<_ n -> ( F ` m ) .c_ ( F ` n ) ) ) : No typesetting found for |- ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) <-> A. m e. A A. n e. A ( m .<_ n -> ( F ` m ) .c_ ( F ` n ) ) ) with typecode |-
62 52 61 sylib Could not format ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> A. m e. A A. n e. A ( m .<_ n -> ( F ` m ) .c_ ( F ` n ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> A. m e. A A. n e. A ( m .<_ n -> ( F ` m ) .c_ ( F ` n ) ) ) with typecode |-
63 51 simprd Could not format ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) with typecode |-
64 breq1 Could not format ( u = i -> ( u .c_ v <-> i .c_ v ) ) : No typesetting found for |- ( u = i -> ( u .c_ v <-> i .c_ v ) ) with typecode |-
65 fveq2 u=iGu=Gi
66 65 breq1d u=iGu˙GvGi˙Gv
67 64 66 imbi12d Could not format ( u = i -> ( ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) <-> ( i .c_ v -> ( G ` i ) .<_ ( G ` v ) ) ) ) : No typesetting found for |- ( u = i -> ( ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) <-> ( i .c_ v -> ( G ` i ) .<_ ( G ` v ) ) ) ) with typecode |-
68 breq2 Could not format ( v = j -> ( i .c_ v <-> i .c_ j ) ) : No typesetting found for |- ( v = j -> ( i .c_ v <-> i .c_ j ) ) with typecode |-
69 fveq2 v=jGv=Gj
70 69 breq2d v=jGi˙GvGi˙Gj
71 68 70 imbi12d Could not format ( v = j -> ( ( i .c_ v -> ( G ` i ) .<_ ( G ` v ) ) <-> ( i .c_ j -> ( G ` i ) .<_ ( G ` j ) ) ) ) : No typesetting found for |- ( v = j -> ( ( i .c_ v -> ( G ` i ) .<_ ( G ` v ) ) <-> ( i .c_ j -> ( G ` i ) .<_ ( G ` j ) ) ) ) with typecode |-
72 67 71 cbvral2vw Could not format ( A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) <-> A. i e. B A. j e. B ( i .c_ j -> ( G ` i ) .<_ ( G ` j ) ) ) : No typesetting found for |- ( A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) <-> A. i e. B A. j e. B ( i .c_ j -> ( G ` i ) .<_ ( G ` j ) ) ) with typecode |-
73 63 72 sylib Could not format ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> A. i e. B A. j e. B ( i .c_ j -> ( G ` i ) .<_ ( G ` j ) ) ) : No typesetting found for |- ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> A. i e. B A. j e. B ( i .c_ j -> ( G ` i ) .<_ ( G ` j ) ) ) with typecode |-
74 id x=mx=m
75 2fveq3 x=mGFx=GFm
76 74 75 breq12d x=mx˙GFxm˙GFm
77 simplr Could not format ( ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) /\ m e. A ) -> A. x e. A x .<_ ( G ` ( F ` x ) ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) /\ m e. A ) -> A. x e. A x .<_ ( G ` ( F ` x ) ) ) with typecode |-
78 simpr Could not format ( ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) /\ m e. A ) -> m e. A ) : No typesetting found for |- ( ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) /\ m e. A ) -> m e. A ) with typecode |-
79 76 77 78 rspcdva Could not format ( ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) /\ m e. A ) -> m .<_ ( G ` ( F ` m ) ) ) : No typesetting found for |- ( ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) /\ m e. A ) -> m .<_ ( G ` ( F ` m ) ) ) with typecode |-
80 2fveq3 u=iFGu=FGi
81 id u=iu=i
82 80 81 breq12d Could not format ( u = i -> ( ( F ` ( G ` u ) ) .c_ u <-> ( F ` ( G ` i ) ) .c_ i ) ) : No typesetting found for |- ( u = i -> ( ( F ` ( G ` u ) ) .c_ u <-> ( F ` ( G ` i ) ) .c_ i ) ) with typecode |-
83 simpllr Could not format ( ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) /\ i e. B ) -> A. u e. B ( F ` ( G ` u ) ) .c_ u ) : No typesetting found for |- ( ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) /\ i e. B ) -> A. u e. B ( F ` ( G ` u ) ) .c_ u ) with typecode |-
84 simpr Could not format ( ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) /\ i e. B ) -> i e. B ) : No typesetting found for |- ( ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) /\ i e. B ) -> i e. B ) with typecode |-
85 82 83 84 rspcdva Could not format ( ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) /\ i e. B ) -> ( F ` ( G ` i ) ) .c_ i ) : No typesetting found for |- ( ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) /\ i e. B ) -> ( F ` ( G ` i ) ) .c_ i ) with typecode |-
86 1 2 3 4 5 46 47 49 50 62 73 79 85 dfmgc2lem Could not format ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> F H G ) : No typesetting found for |- ( ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ A. u e. B ( F ` ( G ` u ) ) .c_ u ) /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) -> F H G ) with typecode |-
87 86 anasss Could not format ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) -> F H G ) : No typesetting found for |- ( ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) -> F H G ) with typecode |-
88 87 anasss Could not format ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) -> F H G ) : No typesetting found for |- ( ( ( ph /\ ( F : A --> B /\ G : B --> A ) ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) -> F H G ) with typecode |-
89 88 anasss Could not format ( ( ph /\ ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) -> F H G ) : No typesetting found for |- ( ( ph /\ ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) -> F H G ) with typecode |-
90 45 89 impbida Could not format ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) ) with typecode |-