Metamath Proof Explorer

Theorem mgcoval

Description: Operation value of the monotone Galois connection. (Contributed by Thierry Arnoux, 23-Apr-2024)

Ref Expression
Hypotheses mgcoval.1 
|- A = ( Base ` V )
mgcoval.2 
|- B = ( Base ` W )
mgcoval.3 
|- .<_ = ( le ` V )
mgcoval.4 
|- .c_ = ( le ` W )
Assertion mgcoval 
|- ( ( V e. X /\ W e. Y ) -> ( V MGalConn W ) = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } )

Proof

Step Hyp Ref Expression
1 mgcoval.1 
 |-  A = ( Base ` V )
2 mgcoval.2 
 |-  B = ( Base ` W )
3 mgcoval.3 
 |-  .<_ = ( le ` V )
4 mgcoval.4 
 |-  .c_ = ( le ` W )
5 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 ) ) ) } )
6 5 a1i 
 |-  ( ( V e. X /\ W e. Y ) -> 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 ) ) ) } ) )
7 fvexd 
 |-  ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) -> ( Base ` v ) e. _V )
8 simprl 
 |-  ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) -> v = V )
9 8 fveq2d 
 |-  ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) -> ( Base ` v ) = ( Base ` V ) )
10 9 1 eqtr4di 
 |-  ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) -> ( Base ` v ) = A )
11 fvexd 
 |-  ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) -> ( Base ` w ) e. _V )
12 simplrr 
 |-  ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) -> w = W )
13 12 fveq2d 
 |-  ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) -> ( Base ` w ) = ( Base ` W ) )
14 13 2 eqtr4di 
 |-  ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) -> ( Base ` w ) = B )
15 simpr 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> b = B )
16 simplr 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> a = A )
17 15 16 oveq12d 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( b ^m a ) = ( B ^m A ) )
18 17 eleq2d 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( f e. ( b ^m a ) <-> f e. ( B ^m A ) ) )
19 16 15 oveq12d 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( a ^m b ) = ( A ^m B ) )
20 19 eleq2d 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( g e. ( a ^m b ) <-> g e. ( A ^m B ) ) )
21 18 20 anbi12d 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( ( f e. ( b ^m a ) /\ g e. ( a ^m b ) ) <-> ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) ) )
22 12 adantr 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> w = W )
23 22 fveq2d 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( le ` w ) = ( le ` W ) )
24 23 4 eqtr4di 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( le ` w ) = .c_ )
25 24 breqd 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( ( f ` x ) ( le ` w ) y <-> ( f ` x ) .c_ y ) )
26 8 ad2antrr 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> v = V )
27 26 fveq2d 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( le ` v ) = ( le ` V ) )
28 27 3 eqtr4di 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( le ` v ) = .<_ )
29 28 breqd 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( x ( le ` v ) ( g ` y ) <-> x .<_ ( g ` y ) ) )
30 25 29 bibi12d 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) <-> ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) )
31 15 30 raleqbidv 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) <-> A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) )
32 16 31 raleqbidv 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( A. x e. a A. y e. b ( ( f ` x ) ( le ` w ) y <-> x ( le ` v ) ( g ` y ) ) <-> A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) )
33 21 32 anbi12d 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = B ) -> ( ( ( 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 ) ) ) <-> ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) )
34 33 opabbidv 
 |-  ( ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = A ) /\ b = 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 ) ) ) } = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } )
35 11 14 34 csbied2 
 |-  ( ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) /\ a = 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 ) ) ) } = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } )
36 7 10 35 csbied2 
 |-  ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) -> [_ ( 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 ) ) ) } = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } )
37 simpl 
 |-  ( ( V e. X /\ W e. Y ) -> V e. X )
38 37 elexd 
 |-  ( ( V e. X /\ W e. Y ) -> V e. _V )
39 simpr 
 |-  ( ( V e. X /\ W e. Y ) -> W e. Y )
40 39 elexd 
 |-  ( ( V e. X /\ W e. Y ) -> W e. _V )
41 ovexd 
 |-  ( ( V e. X /\ W e. Y ) -> ( B ^m A ) e. _V )
42 ovexd 
 |-  ( ( V e. X /\ W e. Y ) -> ( A ^m B ) e. _V )
43 simprll 
 |-  ( ( ( V e. X /\ W e. Y ) /\ ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) -> f e. ( B ^m A ) )
44 simprlr 
 |-  ( ( ( V e. X /\ W e. Y ) /\ ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) ) -> g e. ( A ^m B ) )
45 41 42 43 44 opabex2 
 |-  ( ( V e. X /\ W e. Y ) -> { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } e. _V )
46 6 36 38 40 45 ovmpod 
 |-  ( ( V e. X /\ W e. Y ) -> ( V MGalConn W ) = { <. f , g >. | ( ( f e. ( B ^m A ) /\ g e. ( A ^m B ) ) /\ A. x e. A A. y e. B ( ( f ` x ) .c_ y <-> x .<_ ( g ` y ) ) ) } )