Theorem ismnt

Description: Express the statement " F is monotone". (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	ismnt	|- ( ( V e. X /\ W e. Y ) -> ( F e. ( V Monot W ) <-> ( F : A --> B /\ 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	1 2 3 4	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 ) ) } )
6	5	eleq2d	|- ( ( V e. X /\ W e. Y ) -> ( F e. ( V Monot W ) <-> F e. { f e. ( B ^m A ) | A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) } ) )
7		fveq1	|- ( f = F -> ( f ` x ) = ( F ` x ) )
8		fveq1	|- ( f = F -> ( f ` y ) = ( F ` y ) )
9	7 8	breq12d	|- ( f = F -> ( ( f ` x ) .c_ ( f ` y ) <-> ( F ` x ) .c_ ( F ` y ) ) )
10	9	imbi2d	|- ( f = F -> ( ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) <-> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) )
11	10	2ralbidv	|- ( f = F -> ( A. x e. A A. y e. A ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) <-> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) )
12	11	elrab	|- ( F e. { 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 ) ) ) )
13	6 12	bitrdi	|- ( ( V e. X /\ W e. Y ) -> ( F e. ( V Monot W ) <-> ( F e. ( B ^m A ) /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) )
14	2	fvexi	|- B e. _V
15	1	fvexi	|- A e. _V
16	14 15	elmap	|- ( F e. ( B ^m A ) <-> F : A --> B )
17	16	anbi1i	|- ( ( F e. ( B ^m A ) /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) <-> ( F : A --> B /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) )
18	13 17	bitrdi	|- ( ( V e. X /\ W e. Y ) -> ( F e. ( V Monot W ) <-> ( F : A --> B /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) )