Metamath Proof Explorer

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 
|- 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 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgc 
 |-  MGalConn
1 vv 
 |-  v
2 cvv 
 |-  _V
3 vw 
 |-  w
4 cbs 
 |-  Base
5 1 cv 
 |-  v
6 5 4 cfv 
 |-  ( Base ` v )
7 va 
 |-  a
8 3 cv 
 |-  w
9 8 4 cfv 
 |-  ( Base ` w )
10 vb 
 |-  b
11 vf 
 |-  f
12 vg 
 |-  g
13 11 cv 
 |-  f
14 10 cv 
 |-  b
15 cmap 
 |-  ^m
16 7 cv 
 |-  a
17 14 16 15 co 
 |-  ( b ^m a )
18 13 17 wcel 
 |-  f e. ( b ^m a )
19 12 cv 
 |-  g
20 16 14 15 co 
 |-  ( a ^m b )
21 19 20 wcel 
 |-  g e. ( a ^m b )
22 18 21 wa 
 |-  ( f e. ( b ^m a ) /\ g e. ( a ^m b ) )
23 vx 
 |-  x
24 vy 
 |-  y
25 23 cv 
 |-  x
26 25 13 cfv 
 |-  ( f ` x )
27 cple 
 |-  le
28 8 27 cfv 
 |-  ( le ` w )
29 24 cv 
 |-  y
30 26 29 28 wbr 
 |-  ( f ` x ) ( le ` w ) y
31 5 27 cfv 
 |-  ( le ` v )
32 29 19 cfv 
 |-  ( g ` y )
33 25 32 31 wbr 
 |-  x ( le ` v ) ( g ` y )
34 30 33 wb 
 |-  ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) )
35 34 24 14 wral 
 |-  A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) )
36 35 23 16 wral 
 |-  A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) )
37 22 36 wa 
 |-  ( ( 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 ) ) )
38 37 11 12 copab 
 |-  { <. 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 ) ) ) }
39 10 9 38 csb 
 |-  [_ ( 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 ) ) ) }
40 7 6 39 csb 
 |-  [_ ( 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 ) ) ) }
41 1 3 2 2 40 cmpo 
 |-  ( 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 ) ) ) } )
42 0 41 wceq 
 |-  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 ) ) ) } )