Step | Hyp | Ref
| 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 π |
6 | 2 | cv 1541 |
. . . . 5
class π£ |
7 | | cbs 17088 |
. . . . 5
class
Base |
8 | 6, 7 | cfv 6497 |
. . . 4
class
(Baseβπ£) |
9 | | vx |
. . . . . . . . . 10
setvar π₯ |
10 | 9 | cv 1541 |
. . . . . . . . 9
class π₯ |
11 | | vy |
. . . . . . . . . 10
setvar π¦ |
12 | 11 | cv 1541 |
. . . . . . . . 9
class π¦ |
13 | | cple 17145 |
. . . . . . . . . 10
class
le |
14 | 6, 13 | cfv 6497 |
. . . . . . . . 9
class
(leβπ£) |
15 | 10, 12, 14 | wbr 5106 |
. . . . . . . 8
wff π₯(leβπ£)π¦ |
16 | | vf |
. . . . . . . . . . 11
setvar π |
17 | 16 | cv 1541 |
. . . . . . . . . 10
class π |
18 | 10, 17 | cfv 6497 |
. . . . . . . . 9
class (πβπ₯) |
19 | 12, 17 | cfv 6497 |
. . . . . . . . 9
class (πβπ¦) |
20 | 3 | cv 1541 |
. . . . . . . . . 10
class π€ |
21 | 20, 13 | cfv 6497 |
. . . . . . . . 9
class
(leβπ€) |
22 | 18, 19, 21 | wbr 5106 |
. . . . . . . 8
wff (πβπ₯)(leβπ€)(πβπ¦) |
23 | 15, 22 | wi 4 |
. . . . . . 7
wff (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦)) |
24 | 5 | cv 1541 |
. . . . . . 7
class π |
25 | 23, 11, 24 | wral 3061 |
. . . . . 6
wff
βπ¦ β
π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦)) |
26 | 25, 9, 24 | wral 3061 |
. . . . 5
wff
βπ₯ β
π βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦)) |
27 | 20, 7 | cfv 6497 |
. . . . . 6
class
(Baseβπ€) |
28 | | cmap 8768 |
. . . . . 6
class
βm |
29 | 27, 24, 28 | co 7358 |
. . . . 5
class
((Baseβπ€)
βm π) |
30 | 26, 16, 29 | crab 3406 |
. . . 4
class {π β ((Baseβπ€) βm π) β£ βπ₯ β π βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦))} |
31 | 5, 8, 30 | csb 3856 |
. . 3
class
β¦(Baseβπ£) / πβ¦{π β ((Baseβπ€) βm π) β£ βπ₯ β π βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦))} |
32 | 2, 3, 4, 4, 31 | cmpo 7360 |
. 2
class (π£ β V, π€ β V β¦
β¦(Baseβπ£) / πβ¦{π β ((Baseβπ€) βm π) β£ βπ₯ β π βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦))}) |
33 | 1, 32 | wceq 1542 |
1
wff Monot =
(π£ β V, π€ β V β¦
β¦(Baseβπ£) / πβ¦{π β ((Baseβπ€) βm π) β£ βπ₯ β π βπ¦ β π (π₯(leβπ£)π¦ β (πβπ₯)(leβπ€)(πβπ¦))}) |