Theorem ismnt

Description: Express the statement " F is monotone". (Contributed by Thierry Arnoux, 23-Apr-2024)

	Ref	Expression
Hypotheses	mntoval.1	$$⊢A={\mathrm{Base}}_V$$
	mntoval.2	$$⊢B={\mathrm{Base}}_W$$
	mntoval.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
	mntoval.4	No typesetting found for |- .c_ = ( le ` W ) with typecode |-
Assertion	ismnt	Could not format assertion : No typesetting found for |- ( ( 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 ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mntoval.1	$$⊢A={\mathrm{Base}}_V$$
2		mntoval.2	$$⊢B={\mathrm{Base}}_W$$
3		mntoval.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
4		mntoval.4	Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5	1 2 3 4	mntoval	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 |-
6	5	eleq2d	Could not format ( ( 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 ) ) } ) ) : No typesetting found for |- ( ( 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 ) ) } ) ) with typecode |-
7		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
8		fveq1	$$⊢f=F\to f\left(y\right)=F\left(y\right)$$
9	7 8	breq12d	Could not format ( f = F -> ( ( f ` x ) .c_ ( f ` y ) <-> ( F ` x ) .c_ ( F ` y ) ) ) : No typesetting found for |- ( f = F -> ( ( f ` x ) .c_ ( f ` y ) <-> ( F ` x ) .c_ ( F ` y ) ) ) with typecode |-
10	9	imbi2d	Could not format ( f = F -> ( ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) <-> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) : No typesetting found for |- ( f = F -> ( ( x .<_ y -> ( f ` x ) .c_ ( f ` y ) ) <-> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) with typecode |-
11	10	2ralbidv	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
12	11	elrab	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
13	6 12	bitrdi	Could not format ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) with typecode |-
14	2	fvexi	$$⊢B\in \mathrm{V}$$
15	1	fvexi	$$⊢A\in \mathrm{V}$$
16	14 15	elmap	$$⊢F\in \left(B^A\right)\leftrightarrow F:A⟶B$$
17	16	anbi1i	Could not format ( ( 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 ) ) ) ) : 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 : A --> B /\ A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) ) ) with typecode |-
18	13 17	bitrdi	Could not format ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) with typecode |-