Theorem dfmgc2

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

	Ref	Expression
Hypotheses	mgcoval.1	$$⊢A={\mathrm{Base}}_V$$
	mgcoval.2	$$⊢B={\mathrm{Base}}_W$$
	mgcoval.3	$$⊢\underset{\dot{}}{\le }={\le }_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	$$⊢\phi \to V\in \mathrm{Proset}$$
	mgcval.3	$$⊢\phi \to W\in \mathrm{Proset}$$
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={\mathrm{Base}}_V$$
2		mgcoval.2	$$⊢B={\mathrm{Base}}_W$$
3		mgcoval.3	$$⊢\underset{\dot{}}{\le }={\le }_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	$$⊢\phi \to V\in \mathrm{Proset}$$
7		mgcval.3	$$⊢\phi \to W\in \mathrm{Proset}$$
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	$$⊢\left(\phi \wedge FHG\right)\to \left(F:A⟶B\wedge G:B⟶A\right)$$
10	6	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge FHG\right)\wedge x\in A\right)\wedge y\in A\right)\wedge x\underset{\dot{}}{\le }y\right)\to V\in \mathrm{Proset}$$
11	7	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge FHG\right)\wedge x\in A\right)\wedge y\in A\right)\wedge x\underset{\dot{}}{\le }y\right)\to W\in \mathrm{Proset}$$
12		simp-4r	$$⊢\left(\left(\left(\left(\phi \wedge FHG\right)\wedge x\in A\right)\wedge y\in A\right)\wedge x\underset{\dot{}}{\le }y\right)\to FHG$$
13		simpllr	$$⊢\left(\left(\left(\left(\phi \wedge FHG\right)\wedge x\in A\right)\wedge y\in A\right)\wedge x\underset{\dot{}}{\le }y\right)\to x\in A$$
14		simplr	$$⊢\left(\left(\left(\left(\phi \wedge FHG\right)\wedge x\in A\right)\wedge y\in A\right)\wedge x\underset{\dot{}}{\le }y\right)\to y\in A$$
15		simpr	$$⊢\left(\left(\left(\left(\phi \wedge FHG\right)\wedge x\in A\right)\wedge y\in A\right)\wedge x\underset{\dot{}}{\le }y\right)\to x\underset{\dot{}}{\le }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	$$⊢\left(\left(\phi \wedge FHG\right)\wedge u\in B\right)\to V\in \mathrm{Proset}$$
32	7	ad2antrr	$$⊢\left(\left(\phi \wedge FHG\right)\wedge u\in B\right)\to W\in \mathrm{Proset}$$
33		simplr	$$⊢\left(\left(\phi \wedge FHG\right)\wedge u\in B\right)\to FHG$$
34		simpr	$$⊢\left(\left(\phi \wedge FHG\right)\wedge u\in B\right)\to u\in B$$
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	$$⊢\left(\left(\phi \wedge FHG\right)\wedge x\in A\right)\to V\in \mathrm{Proset}$$
38	7	ad2antrr	$$⊢\left(\left(\phi \wedge FHG\right)\wedge x\in A\right)\to W\in \mathrm{Proset}$$
39		simplr	$$⊢\left(\left(\phi \wedge FHG\right)\wedge x\in A\right)\to FHG$$
40		simpr	$$⊢\left(\left(\phi \wedge FHG\right)\wedge x\in A\right)\to x\in A$$
41	1 2 3 4 5 37 38 39 40	mgccole1	$$⊢\left(\left(\phi \wedge FHG\right)\wedge x\in A\right)\to x\underset{\dot{}}{\le }G\left(F\left(x\right)\right)$$
42	41	ralrimiva	$$⊢\left(\phi \wedge FHG\right)\to \forall x\in Ax\underset{\dot{}}{\le }G\left(F\left(x\right)\right)$$
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=m\to \left(x\underset{\dot{}}{\le }y\leftrightarrow m\underset{\dot{}}{\le }y\right)$$
54		fveq2	$$⊢x=m\to F\left(x\right)=F\left(m\right)$$
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=n\to \left(m\underset{\dot{}}{\le }y\leftrightarrow m\underset{\dot{}}{\le }n\right)$$
58		fveq2	$$⊢y=n\to F\left(y\right)=F\left(n\right)$$
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=i\to G\left(u\right)=G\left(i\right)$$
66	65	breq1d	$$⊢u=i\to \left(G\left(u\right)\underset{\dot{}}{\le }G\left(v\right)\leftrightarrow G\left(i\right)\underset{\dot{}}{\le }G\left(v\right)\right)$$
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=j\to G\left(v\right)=G\left(j\right)$$
70	69	breq2d	$$⊢v=j\to \left(G\left(i\right)\underset{\dot{}}{\le }G\left(v\right)\leftrightarrow G\left(i\right)\underset{\dot{}}{\le }G\left(j\right)\right)$$
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=m\to x=m$$
75		2fveq3	$$⊢x=m\to G\left(F\left(x\right)\right)=G\left(F\left(m\right)\right)$$
76	74 75	breq12d	$$⊢x=m\to \left(x\underset{\dot{}}{\le }G\left(F\left(x\right)\right)\leftrightarrow m\underset{\dot{}}{\le }G\left(F\left(m\right)\right)\right)$$
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=i\to F\left(G\left(u\right)\right)=F\left(G\left(i\right)\right)$$
81		id	$$⊢u=i\to u=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 |-