Definition df-mgc

Description: Define monotone Galois connections. See mgcval for an expanded version. (Contributed by Thierry Arnoux, 20-Apr-2024)

	Ref	Expression
Assertion	df-mgc	Could not format assertion : No typesetting found for |- MGalConn = ( v e. _V , w e. _V |-> [_ ( Base ` v ) / a ]_ [_ ( Base ` w ) / b ]_ { <. f , g >. | ( ( f e. ( b ^m a ) /\ g e. ( a ^m b ) ) /\ A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) ) } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgc	Could not format MGalConn : No typesetting found for class MGalConn with typecode class
1		vv	$$setvarv$$
2		cvv	$$class\mathrm{V}$$
3		vw	$$setvarw$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarv$$
6	5 4	cfv	$$class{\mathrm{Base}}_v$$
7		va	$$setvara$$
8	3	cv	$$setvarw$$
9	8 4	cfv	$$class{\mathrm{Base}}_w$$
10		vb	$$setvarb$$
11		vf	$$setvarf$$
12		vg	$$setvarg$$
13	11	cv	$$setvarf$$
14	10	cv	$$setvarb$$
15		cmap	$$class{\uparrow }_{𝑚}$$
16	7	cv	$$setvara$$
17	14 16 15	co	$$class\left(b^a\right)$$
18	13 17	wcel	$$wfff\in \left(b^a\right)$$
19	12	cv	$$setvarg$$
20	16 14 15	co	$$class\left(a^b\right)$$
21	19 20	wcel	$$wffg\in \left(a^b\right)$$
22	18 21	wa	$$wff\left(f\in \left(b^a\right)\wedge g\in \left(a^b\right)\right)$$
23		vx	$$setvarx$$
24		vy	$$setvary$$
25	23	cv	$$setvarx$$
26	25 13	cfv	$$classf\left(x\right)$$
27		cple	$$class\mathrm{le}$$
28	8 27	cfv	$$class{\le }_w$$
29	24	cv	$$setvary$$
30	26 29 28	wbr	$$wfff\left(x\right){\le }_{w}y$$
31	5 27	cfv	$$class{\le }_v$$
32	29 19	cfv	$$classg\left(y\right)$$
33	25 32 31	wbr	$$wffx{\le }_{v}g\left(y\right)$$
34	30 33	wb	$$wff\left(f\left(x\right){\le }_{w}y\leftrightarrow x{\le }_{v}g\left(y\right)\right)$$
35	34 24 14	wral	$$wff\forall y\in b\left(f\left(x\right){\le }_{w}y\leftrightarrow x{\le }_{v}g\left(y\right)\right)$$
36	35 23 16	wral	$$wff\forall x\in a\forall y\in b\left(f\left(x\right){\le }_{w}y\leftrightarrow x{\le }_{v}g\left(y\right)\right)$$
37	22 36	wa	$$wff\left(\left(f\in \left(b^a\right)\wedge g\in \left(a^b\right)\right)\wedge \forall x\in a\forall y\in b\left(f\left(x\right){\le }_{w}y\leftrightarrow x{\le }_{v}g\left(y\right)\right)\right)$$
38	37 11 12	copab	$$class\left\{⟨f,g⟩|\left(\left(f\in \left(b^a\right)\wedge g\in \left(a^b\right)\right)\wedge \forall x\in a\forall y\in b\left(f\left(x\right){\le }_{w}y\leftrightarrow x{\le }_{v}g\left(y\right)\right)\right)\right\}$$
39	10 9 38	csb	$$class⦋{\mathrm{Base}}_w/b⦌\left\{⟨f,g⟩|\left(\left(f\in \left(b^a\right)\wedge g\in \left(a^b\right)\right)\wedge \forall x\in a\forall y\in b\left(f\left(x\right){\le }_{w}y\leftrightarrow x{\le }_{v}g\left(y\right)\right)\right)\right\}$$
40	7 6 39	csb	$$class⦋{\mathrm{Base}}_v/a⦌⦋{\mathrm{Base}}_w/b⦌\left\{⟨f,g⟩|\left(\left(f\in \left(b^a\right)\wedge g\in \left(a^b\right)\right)\wedge \forall x\in a\forall y\in b\left(f\left(x\right){\le }_{w}y\leftrightarrow x{\le }_{v}g\left(y\right)\right)\right)\right\}$$
41	1 3 2 2 40	cmpo	$$class\left(v\in \mathrm{V},w\in \mathrm{V}⟼⦋{\mathrm{Base}}_v/a⦌⦋{\mathrm{Base}}_w/b⦌\left\{⟨f,g⟩|\left(\left(f\in \left(b^a\right)\wedge g\in \left(a^b\right)\right)\wedge \forall x\in a\forall y\in b\left(f\left(x\right){\le }_{w}y\leftrightarrow x{\le }_{v}g\left(y\right)\right)\right)\right\}\right)$$
42	0 41	wceq	Could not format MGalConn = ( v e. _V , w e. _V |-> [_ ( Base ` v ) / a ]_ [_ ( Base ` w ) / b ]_ { <. f , g >. | ( ( f e. ( b ^m a ) /\ g e. ( a ^m b ) ) /\ A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) ) } ) : No typesetting found for wff MGalConn = ( v e. _V , w e. _V |-> [_ ( Base ` v ) / a ]_ [_ ( Base ` w ) / b ]_ { <. f , g >. | ( ( f e. ( b ^m a ) /\ g e. ( a ^m b ) ) /\ A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) ) } ) with typecode wff