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

Proof

Step Hyp Ref Expression
1 mntoval.1 A = Base V
2 mntoval.2 B = Base W
3 mntoval.3 ˙ = V
4 mntoval.4 Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5 df-mnt Could not format 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 ) ) } ) : No typesetting found for |- 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 ) ) } ) with typecode |-
6 5 a1i Could not format ( ( 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 ) ) } ) ) : No typesetting found for |- ( ( 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 ) ) } ) ) with typecode |-
7 fvexd v = V w = W Base v 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 a = B A
16 simpll v = V w = W a = A v = V
17 16 fveq2d v = V w = W a = A v = V
18 17 3 eqtr4di v = V w = W a = A v = ˙
19 18 breqd v = V w = W a = A x v y x ˙ y
20 11 fveq2d v = V w = W a = A w = W
21 20 4 eqtr4di Could not format ( ( ( v = V /\ w = W ) /\ a = A ) -> ( le ` w ) = .c_ ) : No typesetting found for |- ( ( ( v = V /\ w = W ) /\ a = A ) -> ( le ` w ) = .c_ ) with typecode |-
22 21 breqd Could not format ( ( ( v = V /\ w = W ) /\ a = A ) -> ( ( f ` x ) ( le ` w ) ( f ` y ) <-> ( f ` x ) .c_ ( f ` y ) ) ) : No typesetting found for |- ( ( ( v = V /\ w = W ) /\ a = A ) -> ( ( f ` x ) ( le ` w ) ( f ` y ) <-> ( f ` x ) .c_ ( f ` y ) ) ) with typecode |-
23 19 22 imbi12d Could not format ( ( ( v = V /\ w = W ) /\ a = A ) -> ( ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) <-> ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) ) ) : No typesetting found for |- ( ( ( v = V /\ w = W ) /\ a = A ) -> ( ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) <-> ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) ) ) with typecode |-
24 14 23 raleqbidv Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
25 14 24 raleqbidv Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
26 15 25 rabeqbidv Could not format ( ( ( 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 ) ) } ) : No typesetting found for |- ( ( ( 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 ) ) } ) with typecode |-
27 7 10 26 csbied2 Could not format ( ( 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 ) ) } ) : No typesetting found for |- ( ( 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 ) ) } ) with typecode |-
28 27 adantl Could not format ( ( ( 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 ) ) } ) : No typesetting found for |- ( ( ( 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 ) ) } ) with typecode |-
29 elex V X V V
30 29 adantr V X W Y V V
31 elex W Y W V
32 31 adantl V X W Y W V
33 eqid Could not format { 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 ) ) } : No typesetting found for |- { 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 ) ) } with typecode |-
34 ovexd V X W Y B A V
35 33 34 rabexd Could not format ( ( 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 ) : No typesetting found for |- ( ( 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 ) with typecode |-
36 6 28 30 32 35 ovmpod Could not format ( ( 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 ) ) } ) : No typesetting found for |- ( ( 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 ) ) } ) with typecode |-