Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mnt Structured version   Visualization version   GIF version

Definition df-mnt 30688
 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
StepHypRef Expression
1 cmnt 30686 . 2 class Monot
2 vv . . 3 setvar 𝑣
3 vw . . 3 setvar 𝑤
4 cvv 3441 . . 3 class V
5 va . . . 4 setvar 𝑎
62cv 1537 . . . . 5 class 𝑣
7 cbs 16475 . . . . 5 class Base
86, 7cfv 6324 . . . 4 class (Base‘𝑣)
9 vx . . . . . . . . . 10 setvar 𝑥
109cv 1537 . . . . . . . . 9 class 𝑥
11 vy . . . . . . . . . 10 setvar 𝑦
1211cv 1537 . . . . . . . . 9 class 𝑦
13 cple 16564 . . . . . . . . . 10 class le
146, 13cfv 6324 . . . . . . . . 9 class (le‘𝑣)
1510, 12, 14wbr 5030 . . . . . . . 8 wff 𝑥(le‘𝑣)𝑦
16 vf . . . . . . . . . . 11 setvar 𝑓
1716cv 1537 . . . . . . . . . 10 class 𝑓
1810, 17cfv 6324 . . . . . . . . 9 class (𝑓𝑥)
1912, 17cfv 6324 . . . . . . . . 9 class (𝑓𝑦)
203cv 1537 . . . . . . . . . 10 class 𝑤
2120, 13cfv 6324 . . . . . . . . 9 class (le‘𝑤)
2218, 19, 21wbr 5030 . . . . . . . 8 wff (𝑓𝑥)(le‘𝑤)(𝑓𝑦)
2315, 22wi 4 . . . . . . 7 wff (𝑥(le‘𝑣)𝑦 → (𝑓𝑥)(le‘𝑤)(𝑓𝑦))
245cv 1537 . . . . . . 7 class 𝑎
2523, 11, 24wral 3106 . . . . . 6 wff 𝑦𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓𝑥)(le‘𝑤)(𝑓𝑦))
2625, 9, 24wral 3106 . . . . 5 wff 𝑥𝑎𝑦𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓𝑥)(le‘𝑤)(𝑓𝑦))
2720, 7cfv 6324 . . . . . 6 class (Base‘𝑤)
28 cmap 8389 . . . . . 6 class m
2927, 24, 28co 7135 . . . . 5 class ((Base‘𝑤) ↑m 𝑎)
3026, 16, 29crab 3110 . . . 4 class {𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥𝑎𝑦𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓𝑥)(le‘𝑤)(𝑓𝑦))}
315, 8, 30csb 3828 . . 3 class (Base‘𝑣) / 𝑎{𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥𝑎𝑦𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓𝑥)(le‘𝑤)(𝑓𝑦))}
322, 3, 4, 4, 31cmpo 7137 . 2 class (𝑣 ∈ V, 𝑤 ∈ V ↦ (Base‘𝑣) / 𝑎{𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥𝑎𝑦𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓𝑥)(le‘𝑤)(𝑓𝑦))})
331, 32wceq 1538 1 wff Monot = (𝑣 ∈ V, 𝑤 ∈ V ↦ (Base‘𝑣) / 𝑎{𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥𝑎𝑦𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓𝑥)(le‘𝑤)(𝑓𝑦))})
 Colors of variables: wff setvar class This definition is referenced by:  mntoval  30690
 Copyright terms: Public domain W3C validator