Detailed syntax breakdown of Definition df-mnt
Step | Hyp | Ref
| Expression |
1 | | cmnt 30767 |
. 2
class
Monot |
2 | | vv |
. . 3
setvar 𝑣 |
3 | | vw |
. . 3
setvar 𝑤 |
4 | | cvv 3407 |
. . 3
class
V |
5 | | va |
. . . 4
setvar 𝑎 |
6 | 2 | cv 1538 |
. . . . 5
class 𝑣 |
7 | | cbs 16526 |
. . . . 5
class
Base |
8 | 6, 7 | cfv 6328 |
. . . 4
class
(Base‘𝑣) |
9 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
10 | 9 | cv 1538 |
. . . . . . . . 9
class 𝑥 |
11 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
12 | 11 | cv 1538 |
. . . . . . . . 9
class 𝑦 |
13 | | cple 16615 |
. . . . . . . . . 10
class
le |
14 | 6, 13 | cfv 6328 |
. . . . . . . . 9
class
(le‘𝑣) |
15 | 10, 12, 14 | wbr 5025 |
. . . . . . . 8
wff 𝑥(le‘𝑣)𝑦 |
16 | | vf |
. . . . . . . . . . 11
setvar 𝑓 |
17 | 16 | cv 1538 |
. . . . . . . . . 10
class 𝑓 |
18 | 10, 17 | cfv 6328 |
. . . . . . . . 9
class (𝑓‘𝑥) |
19 | 12, 17 | cfv 6328 |
. . . . . . . . 9
class (𝑓‘𝑦) |
20 | 3 | cv 1538 |
. . . . . . . . . 10
class 𝑤 |
21 | 20, 13 | cfv 6328 |
. . . . . . . . 9
class
(le‘𝑤) |
22 | 18, 19, 21 | wbr 5025 |
. . . . . . . 8
wff (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦) |
23 | 15, 22 | wi 4 |
. . . . . . 7
wff (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦)) |
24 | 5 | cv 1538 |
. . . . . . 7
class 𝑎 |
25 | 23, 11, 24 | wral 3068 |
. . . . . 6
wff
∀𝑦 ∈
𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦)) |
26 | 25, 9, 24 | wral 3068 |
. . . . 5
wff
∀𝑥 ∈
𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦)) |
27 | 20, 7 | cfv 6328 |
. . . . . 6
class
(Base‘𝑤) |
28 | | cmap 8409 |
. . . . . 6
class
↑m |
29 | 27, 24, 28 | co 7143 |
. . . . 5
class
((Base‘𝑤)
↑m 𝑎) |
30 | 26, 16, 29 | crab 3072 |
. . . 4
class {𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))} |
31 | 5, 8, 30 | csb 3801 |
. . 3
class
⦋(Base‘𝑣) / 𝑎⦌{𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))} |
32 | 2, 3, 4, 4, 31 | cmpo 7145 |
. 2
class (𝑣 ∈ V, 𝑤 ∈ V ↦
⦋(Base‘𝑣) / 𝑎⦌{𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))}) |
33 | 1, 32 | wceq 1539 |
1
wff Monot =
(𝑣 ∈ V, 𝑤 ∈ V ↦
⦋(Base‘𝑣) / 𝑎⦌{𝑓 ∈ ((Base‘𝑤) ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑎 (𝑥(le‘𝑣)𝑦 → (𝑓‘𝑥)(le‘𝑤)(𝑓‘𝑦))}) |