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 ˙ = V
mgcoval.4 No typesetting found for |- .c_ = ( le ` W ) with typecode |-
Assertion mgcoval Could not format assertion : No typesetting found for |- ( ( 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 ) ) ) } ) with typecode |-

Proof

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