Metamath Proof Explorer

Definition df-mnt

Description: Define a monotone function between two ordered sets. (Contributed by Thierry Arnoux, 20-Apr-2024)

Ref Expression
Assertion 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 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmnt 
 |-  Monot
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 vf 
 |-  f
9 3 cv 
 |-  w
10 9 4 cfv 
 |-  ( Base ` w )
11 cmap 
 |-  ^m
12 7 cv 
 |-  a
13 10 12 11 co 
 |-  ( ( Base ` w ) ^m a )
14 vx 
 |-  x
15 vy 
 |-  y
16 14 cv 
 |-  x
17 cple 
 |-  le
18 5 17 cfv 
 |-  ( le ` v )
19 15 cv 
 |-  y
20 16 19 18 wbr 
 |-  x ( le ` v ) y
21 8 cv 
 |-  f
22 16 21 cfv 
 |-  ( f ` x )
23 9 17 cfv 
 |-  ( le ` w )
24 19 21 cfv 
 |-  ( f ` y )
25 22 24 23 wbr 
 |-  ( f ` x ) ( le ` w ) ( f ` y )
26 20 25 wi 
 |-  ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) )
27 26 15 12 wral 
 |-  A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) )
28 27 14 12 wral 
 |-  A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) )
29 28 8 13 crab 
 |-  { f e. ( ( Base ` w ) ^m a ) | A. x e. a A. y e. a ( x ( le ` v ) y -> ( f ` x ) ( le ` w ) ( f ` y ) ) }
30 7 6 29 csb 
 |-  [_ ( 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 ) ) }
31 1 3 2 2 30 cmpo 
 |-  ( 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 ) ) } )
32 0 31 wceq 
 |-  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 ) ) } )