Definition df-mnt 30931

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

Assertion

Ref	Expression
df-mnt	⊢ Monot = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌{𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))})

Distinct variable group:   𝑓,𝑎,𝑣,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-mnt

Step	Hyp	Ref	Expression
1		cmnt 30929	. 2 class Monot
2		vv	. . 3 setvar 𝑣
3		vw	. . 3 setvar 𝑤
4		cvv 3398	. . 3 class V
5		va	. . . 4 setvar 𝑎
6	2	cv 1542	. . . . 5 class 𝑣
7		cbs 16666	. . . . 5 class Base
8	6, 7	cfv 6358	. . . 4 class (Base‘𝑣)
9		vx	. . . . . . . . . 10 setvar 𝑥
10	9	cv 1542	. . . . . . . . 9 class 𝑥
11		vy	. . . . . . . . . 10 setvar 𝑦
12	11	cv 1542	. . . . . . . . 9 class 𝑦
13		cple 16756	. . . . . . . . . 10 class le
14	6, 13	cfv 6358	. . . . . . . . 9 class (le‘𝑣)
15	10, 12, 14	wbr 5039	. . . . . . . 8 wff 𝑥(le‘𝑣)𝑦
16		vf	. . . . . . . . . . 11 setvar 𝑓
17	16	cv 1542	. . . . . . . . . 10 class 𝑓
18	10, 17	cfv 6358	. . . . . . . . 9 class (𝑓‘𝑥)
19	12, 17	cfv 6358	. . . . . . . . 9 class (𝑓‘𝑦)
20	3	cv 1542	. . . . . . . . . 10 class 𝑤
21	20, 13	cfv 6358	. . . . . . . . 9 class (le‘𝑤)
22	18, 19, 21	wbr 5039	. . . . . . . 8 wff (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦)
23	15, 22	wi 4	. . . . . . 7 wff (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))
24	5	cv 1542	. . . . . . 7 class 𝑎
25	23, 11, 24	wral 3051	. . . . . 6 wff ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))
26	25, 9, 24	wral 3051	. . . . 5 wff ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))
27	20, 7	cfv 6358	. . . . . 6 class (Base‘𝑤)
28		cmap 8486	. . . . . 6 class ↑m
29	27, 24, 28	co 7191	. . . . 5 class ((Base‘𝑤) ↑m 𝑎)
30	26, 16, 29	crab 3055	. . . 4 class {𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))}
31	5, 8, 30	csb 3798	. . 3 class ⦋(Base‘𝑣) / 𝑎⦌{𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))}
32	2, 3, 4, 4, 31	cmpo 7193	. 2 class (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌{𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))})
33	1, 32	wceq 1543	1 wff Monot = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(Base‘𝑣) / 𝑎⦌{𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))})

This definition is referenced by:  mntoval  30933