This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) ) )