Metamath Proof Explorer

Theorem mntoval

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

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

Proof

Step Hyp Ref Expression
1 mntoval.1 
 |-  A = ( Base ` V )
2 mntoval.2 
 |-  B = ( Base ` W )
3 mntoval.3 
 |-  .<_ = ( le ` V )
4 mntoval.4 
 |-  .c_ = ( le ` W )
5 df-mnt 
 |-  Monot = ( v e. _V , w e. _V |-> [_ ( Base ` v ) / a ]_ { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } )
6 5 a1i 
 |-  ( ( V e. X /\ W e. Y ) -> Monot = ( v e. _V , w e. _V |-> [_ ( Base ` v ) / a ]_ { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } ) )
7 fvexd 
 |-  ( ( v = V /\ w = W ) -> ( Base ` v ) e. _V )
8 fveq2 
 |-  ( v = V -> ( Base ` v ) = ( Base ` V ) )
9 8 1 eqtr4di 
 |-  ( v = V -> ( Base ` v ) = A )
10 9 adantr 
 |-  ( ( v = V /\ w = W ) -> ( Base ` v ) = A )
11 simplr 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> w = W )
12 11 fveq2d 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> ( Base ` w ) = ( Base ` W ) )
13 12 2 eqtr4di 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> ( Base ` w ) = B )
14 simpr 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> a = A )
15 13 14 oveq12d 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> ( ( Base ` w ) ^m a ) = ( B ^m A ) )
16 simpll 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> v = V )
17 16 fveq2d 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> ( le ` v ) = ( le ` V ) )
18 17 3 eqtr4di 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> ( le ` v ) = .<_ )
19 18 breqd 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> ( x ( le ` v ) y <-> x .<_ y ) )
20 11 fveq2d 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> ( le ` w ) = ( le ` W ) )
21 20 4 eqtr4di 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> ( le ` w ) = .c_ )
22 21 breqd 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> ( ( f ` x ) ( le ` w ) ( f ` y ) <-> ( f ` x ) .c_ ( f ` y ) ) )
23 19 22 imbi12d 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> ( ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) <-> ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) ) )
24 14 23 raleqbidv 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> ( A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) <-> A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) ) )
25 14 24 raleqbidv 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> ( A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) <-> A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) ) )
26 15 25 rabeqbidv 
 |-  ( ( ( v = V /\ w = W ) /\ a = A ) -> { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } )
27 7 10 26 csbied2 
 |-  ( ( v = V /\ w = W ) -> [_ ( Base ` v ) / a ]_ { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } )
28 27 adantl 
 |-  ( ( ( V e. X /\ W e. Y ) /\ ( v = V /\ w = W ) ) -> [_ ( Base ` v ) / a ]_ { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) } = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } )
29 elex 
 |-  ( V e. X -> V e. _V )
30 29 adantr 
 |-  ( ( V e. X /\ W e. Y ) -> V e. _V )
31 elex 
 |-  ( W e. Y -> W e. _V )
32 31 adantl 
 |-  ( ( V e. X /\ W e. Y ) -> W e. _V )
33 eqid 
 |-  { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) }
34 ovexd 
 |-  ( ( V e. X /\ W e. Y ) -> ( B ^m A ) e. _V )
35 33 34 rabexd 
 |-  ( ( V e. X /\ W e. Y ) -> { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } e. _V )
36 6 28 30 32 35 ovmpod 
 |-  ( ( V e. X /\ W e. Y ) -> ( V Monot W ) = { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } )