Step | Hyp | Ref
| Expression |
1 | | culm 25719 |
. 2
class
βπ’ |
2 | | vs |
. . 3
setvar π |
3 | | cvv 3443 |
. . 3
class
V |
4 | | vn |
. . . . . . . . 9
setvar π |
5 | 4 | cv 1540 |
. . . . . . . 8
class π |
6 | | cuz 12759 |
. . . . . . . 8
class
β€β₯ |
7 | 5, 6 | cfv 6493 |
. . . . . . 7
class
(β€β₯βπ) |
8 | | cc 11045 |
. . . . . . . 8
class
β |
9 | 2 | cv 1540 |
. . . . . . . 8
class π |
10 | | cmap 8761 |
. . . . . . . 8
class
βm |
11 | 8, 9, 10 | co 7353 |
. . . . . . 7
class (β
βm π ) |
12 | | vf |
. . . . . . . 8
setvar π |
13 | 12 | cv 1540 |
. . . . . . 7
class π |
14 | 7, 11, 13 | wf 6489 |
. . . . . 6
wff π:(β€β₯βπ)βΆ(β
βm π ) |
15 | | vy |
. . . . . . . 8
setvar π¦ |
16 | 15 | cv 1540 |
. . . . . . 7
class π¦ |
17 | 9, 8, 16 | wf 6489 |
. . . . . 6
wff π¦:π βΆβ |
18 | | vz |
. . . . . . . . . . . . . . 15
setvar π§ |
19 | 18 | cv 1540 |
. . . . . . . . . . . . . 14
class π§ |
20 | | vk |
. . . . . . . . . . . . . . . 16
setvar π |
21 | 20 | cv 1540 |
. . . . . . . . . . . . . . 15
class π |
22 | 21, 13 | cfv 6493 |
. . . . . . . . . . . . . 14
class (πβπ) |
23 | 19, 22 | cfv 6493 |
. . . . . . . . . . . . 13
class ((πβπ)βπ§) |
24 | 19, 16 | cfv 6493 |
. . . . . . . . . . . . 13
class (π¦βπ§) |
25 | | cmin 11381 |
. . . . . . . . . . . . 13
class
β |
26 | 23, 24, 25 | co 7353 |
. . . . . . . . . . . 12
class (((πβπ)βπ§) β (π¦βπ§)) |
27 | | cabs 15111 |
. . . . . . . . . . . 12
class
abs |
28 | 26, 27 | cfv 6493 |
. . . . . . . . . . 11
class
(absβ(((πβπ)βπ§) β (π¦βπ§))) |
29 | | vx |
. . . . . . . . . . . 12
setvar π₯ |
30 | 29 | cv 1540 |
. . . . . . . . . . 11
class π₯ |
31 | | clt 11185 |
. . . . . . . . . . 11
class
< |
32 | 28, 30, 31 | wbr 5103 |
. . . . . . . . . 10
wff
(absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯ |
33 | 32, 18, 9 | wral 3062 |
. . . . . . . . 9
wff
βπ§ β
π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯ |
34 | | vj |
. . . . . . . . . . 11
setvar π |
35 | 34 | cv 1540 |
. . . . . . . . . 10
class π |
36 | 35, 6 | cfv 6493 |
. . . . . . . . 9
class
(β€β₯βπ) |
37 | 33, 20, 36 | wral 3062 |
. . . . . . . 8
wff
βπ β
(β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯ |
38 | 37, 34, 7 | wrex 3071 |
. . . . . . 7
wff
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯ |
39 | | crp 12907 |
. . . . . . 7
class
β+ |
40 | 38, 29, 39 | wral 3062 |
. . . . . 6
wff
βπ₯ β
β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯ |
41 | 14, 17, 40 | w3a 1087 |
. . . . 5
wff (π:(β€β₯βπ)βΆ(β
βm π ) β§
π¦:π βΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯) |
42 | | cz 12495 |
. . . . 5
class
β€ |
43 | 41, 4, 42 | wrex 3071 |
. . . 4
wff
βπ β
β€ (π:(β€β₯βπ)βΆ(β
βm π ) β§
π¦:π βΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯) |
44 | 43, 12, 15 | copab 5165 |
. . 3
class
{β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π ) β§
π¦:π βΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)} |
45 | 2, 3, 44 | cmpt 5186 |
. 2
class (π β V β¦ {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π ) β§
π¦:π βΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)}) |
46 | 1, 45 | wceq 1541 |
1
wff
βπ’ = (π β V β¦ {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β
βm π ) β§
π¦:π βΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)}) |