Users' Mathboxes 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 31889
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 31887 . 2 class Monot
2 vv . . 3 setvar 𝑣
3 vw . . 3 setvar 𝑀
4 cvv 3444 . . 3 class V
5 va . . . 4 setvar π‘Ž
62cv 1541 . . . . 5 class 𝑣
7 cbs 17088 . . . . 5 class Base
86, 7cfv 6497 . . . 4 class (Baseβ€˜π‘£)
9 vx . . . . . . . . . 10 setvar π‘₯
109cv 1541 . . . . . . . . 9 class π‘₯
11 vy . . . . . . . . . 10 setvar 𝑦
1211cv 1541 . . . . . . . . 9 class 𝑦
13 cple 17145 . . . . . . . . . 10 class le
146, 13cfv 6497 . . . . . . . . 9 class (leβ€˜π‘£)
1510, 12, 14wbr 5106 . . . . . . . 8 wff π‘₯(leβ€˜π‘£)𝑦
16 vf . . . . . . . . . . 11 setvar 𝑓
1716cv 1541 . . . . . . . . . 10 class 𝑓
1810, 17cfv 6497 . . . . . . . . 9 class (π‘“β€˜π‘₯)
1912, 17cfv 6497 . . . . . . . . 9 class (π‘“β€˜π‘¦)
203cv 1541 . . . . . . . . . 10 class 𝑀
2120, 13cfv 6497 . . . . . . . . 9 class (leβ€˜π‘€)
2218, 19, 21wbr 5106 . . . . . . . 8 wff (π‘“β€˜π‘₯)(leβ€˜π‘€)(π‘“β€˜π‘¦)
2315, 22wi 4 . . . . . . 7 wff (π‘₯(leβ€˜π‘£)𝑦 β†’ (π‘“β€˜π‘₯)(leβ€˜π‘€)(π‘“β€˜π‘¦))
245cv 1541 . . . . . . 7 class π‘Ž
2523, 11, 24wral 3061 . . . . . 6 wff βˆ€π‘¦ ∈ π‘Ž (π‘₯(leβ€˜π‘£)𝑦 β†’ (π‘“β€˜π‘₯)(leβ€˜π‘€)(π‘“β€˜π‘¦))
2625, 9, 24wral 3061 . . . . 5 wff βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ π‘Ž (π‘₯(leβ€˜π‘£)𝑦 β†’ (π‘“β€˜π‘₯)(leβ€˜π‘€)(π‘“β€˜π‘¦))
2720, 7cfv 6497 . . . . . 6 class (Baseβ€˜π‘€)
28 cmap 8768 . . . . . 6 class ↑m
2927, 24, 28co 7358 . . . . 5 class ((Baseβ€˜π‘€) ↑m π‘Ž)
3026, 16, 29crab 3406 . . . 4 class {𝑓 ∈ ((Baseβ€˜π‘€) ↑m π‘Ž) ∣ βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ π‘Ž (π‘₯(leβ€˜π‘£)𝑦 β†’ (π‘“β€˜π‘₯)(leβ€˜π‘€)(π‘“β€˜π‘¦))}
315, 8, 30csb 3856 . . 3 class ⦋(Baseβ€˜π‘£) / π‘Žβ¦Œ{𝑓 ∈ ((Baseβ€˜π‘€) ↑m π‘Ž) ∣ βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ π‘Ž (π‘₯(leβ€˜π‘£)𝑦 β†’ (π‘“β€˜π‘₯)(leβ€˜π‘€)(π‘“β€˜π‘¦))}
322, 3, 4, 4, 31cmpo 7360 . 2 class (𝑣 ∈ V, 𝑀 ∈ V ↦ ⦋(Baseβ€˜π‘£) / π‘Žβ¦Œ{𝑓 ∈ ((Baseβ€˜π‘€) ↑m π‘Ž) ∣ βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ π‘Ž (π‘₯(leβ€˜π‘£)𝑦 β†’ (π‘“β€˜π‘₯)(leβ€˜π‘€)(π‘“β€˜π‘¦))})
331, 32wceq 1542 1 wff Monot = (𝑣 ∈ V, 𝑀 ∈ V ↦ ⦋(Baseβ€˜π‘£) / π‘Žβ¦Œ{𝑓 ∈ ((Baseβ€˜π‘€) ↑m π‘Ž) ∣ βˆ€π‘₯ ∈ π‘Ž βˆ€π‘¦ ∈ π‘Ž (π‘₯(leβ€˜π‘£)𝑦 β†’ (π‘“β€˜π‘₯)(leβ€˜π‘€)(π‘“β€˜π‘¦))})
Colors of variables: wff setvar class
This definition is referenced by:  mntoval  31891
  Copyright terms: Public domain W3C validator