Definition df-mnt

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

	Ref	Expression
Assertion	df-mnt	$$⊢\mathrm{Monot}=\left(v\in \mathrm{V},w\in \mathrm{V}⟼⦋{\mathrm{Base}}_v/a⦌\left\{f\in \left({{\mathrm{Base}}_w}^a\right)|\forall x\in a\forall y\in a\left(x{\le }_{v}y\to f\left(x\right){\le }_{w}f\left(y\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmnt	$$class\mathrm{Monot}$$
1		vv	$$setvarv$$
2		cvv	$$class\mathrm{V}$$
3		vw	$$setvarw$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarv$$
6	5 4	cfv	$$class{\mathrm{Base}}_v$$
7		va	$$setvara$$
8		vf	$$setvarf$$
9	3	cv	$$setvarw$$
10	9 4	cfv	$$class{\mathrm{Base}}_w$$
11		cmap	$$class{\uparrow }_{𝑚}$$
12	7	cv	$$setvara$$
13	10 12 11	co	$$class\left({{\mathrm{Base}}_w}^a\right)$$
14		vx	$$setvarx$$
15		vy	$$setvary$$
16	14	cv	$$setvarx$$
17		cple	$$class\mathrm{le}$$
18	5 17	cfv	$$class{\le }_v$$
19	15	cv	$$setvary$$
20	16 19 18	wbr	$$wffx{\le }_{v}y$$
21	8	cv	$$setvarf$$
22	16 21	cfv	$$classf\left(x\right)$$
23	9 17	cfv	$$class{\le }_w$$
24	19 21	cfv	$$classf\left(y\right)$$
25	22 24 23	wbr	$$wfff\left(x\right){\le }_{w}f\left(y\right)$$
26	20 25	wi	$$wff\left(x{\le }_{v}y\to f\left(x\right){\le }_{w}f\left(y\right)\right)$$
27	26 15 12	wral	$$wff\forall y\in a\left(x{\le }_{v}y\to f\left(x\right){\le }_{w}f\left(y\right)\right)$$
28	27 14 12	wral	$$wff\forall x\in a\forall y\in a\left(x{\le }_{v}y\to f\left(x\right){\le }_{w}f\left(y\right)\right)$$
29	28 8 13	crab	$$class\left\{f\in \left({{\mathrm{Base}}_w}^a\right)|\forall x\in a\forall y\in a\left(x{\le }_{v}y\to f\left(x\right){\le }_{w}f\left(y\right)\right)\right\}$$
30	7 6 29	csb	$$class⦋{\mathrm{Base}}_v/a⦌\left\{f\in \left({{\mathrm{Base}}_w}^a\right)|\forall x\in a\forall y\in a\left(x{\le }_{v}y\to f\left(x\right){\le }_{w}f\left(y\right)\right)\right\}$$
31	1 3 2 2 30	cmpo	$$class\left(v\in \mathrm{V},w\in \mathrm{V}⟼⦋{\mathrm{Base}}_v/a⦌\left\{f\in \left({{\mathrm{Base}}_w}^a\right)|\forall x\in a\forall y\in a\left(x{\le }_{v}y\to f\left(x\right){\le }_{w}f\left(y\right)\right)\right\}\right)$$
32	0 31	wceq	$$wff\mathrm{Monot}=\left(v\in \mathrm{V},w\in \mathrm{V}⟼⦋{\mathrm{Base}}_v/a⦌\left\{f\in \left({{\mathrm{Base}}_w}^a\right)|\forall x\in a\forall y\in a\left(x{\le }_{v}y\to f\left(x\right){\le }_{w}f\left(y\right)\right)\right\}\right)$$