Step | Hyp | Ref
| Expression |
1 | | crpm 20142 |
. 2
class
RPrime |
2 | | vw |
. . 3
setvar π€ |
3 | | cvv 3446 |
. . 3
class
V |
4 | | vb |
. . . 4
setvar π |
5 | 2 | cv 1541 |
. . . . 5
class π€ |
6 | | cbs 17084 |
. . . . 5
class
Base |
7 | 5, 6 | cfv 6497 |
. . . 4
class
(Baseβπ€) |
8 | | vp |
. . . . . . . . . . 11
setvar π |
9 | 8 | cv 1541 |
. . . . . . . . . 10
class π |
10 | | vx |
. . . . . . . . . . . 12
setvar π₯ |
11 | 10 | cv 1541 |
. . . . . . . . . . 11
class π₯ |
12 | | vy |
. . . . . . . . . . . 12
setvar π¦ |
13 | 12 | cv 1541 |
. . . . . . . . . . 11
class π¦ |
14 | | cmulr 17135 |
. . . . . . . . . . . 12
class
.r |
15 | 5, 14 | cfv 6497 |
. . . . . . . . . . 11
class
(.rβπ€) |
16 | 11, 13, 15 | co 7358 |
. . . . . . . . . 10
class (π₯(.rβπ€)π¦) |
17 | | vd |
. . . . . . . . . . 11
setvar π |
18 | 17 | cv 1541 |
. . . . . . . . . 10
class π |
19 | 9, 16, 18 | wbr 5106 |
. . . . . . . . 9
wff ππ(π₯(.rβπ€)π¦) |
20 | 9, 11, 18 | wbr 5106 |
. . . . . . . . . 10
wff πππ₯ |
21 | 9, 13, 18 | wbr 5106 |
. . . . . . . . . 10
wff πππ¦ |
22 | 20, 21 | wo 846 |
. . . . . . . . 9
wff (πππ₯ β¨ πππ¦) |
23 | 19, 22 | wi 4 |
. . . . . . . 8
wff (ππ(π₯(.rβπ€)π¦) β (πππ₯ β¨ πππ¦)) |
24 | | cdsr 20068 |
. . . . . . . . 9
class
β₯r |
25 | 5, 24 | cfv 6497 |
. . . . . . . 8
class
(β₯rβπ€) |
26 | 23, 17, 25 | wsbc 3740 |
. . . . . . 7
wff
[(β₯rβπ€) / π](ππ(π₯(.rβπ€)π¦) β (πππ₯ β¨ πππ¦)) |
27 | 4 | cv 1541 |
. . . . . . 7
class π |
28 | 26, 12, 27 | wral 3065 |
. . . . . 6
wff
βπ¦ β
π
[(β₯rβπ€) / π](ππ(π₯(.rβπ€)π¦) β (πππ₯ β¨ πππ¦)) |
29 | 28, 10, 27 | wral 3065 |
. . . . 5
wff
βπ₯ β
π βπ¦ β π [(β₯rβπ€) / π](ππ(π₯(.rβπ€)π¦) β (πππ₯ β¨ πππ¦)) |
30 | | cui 20069 |
. . . . . . . 8
class
Unit |
31 | 5, 30 | cfv 6497 |
. . . . . . 7
class
(Unitβπ€) |
32 | | c0g 17322 |
. . . . . . . . 9
class
0g |
33 | 5, 32 | cfv 6497 |
. . . . . . . 8
class
(0gβπ€) |
34 | 33 | csn 4587 |
. . . . . . 7
class
{(0gβπ€)} |
35 | 31, 34 | cun 3909 |
. . . . . 6
class
((Unitβπ€)
βͺ {(0gβπ€)}) |
36 | 27, 35 | cdif 3908 |
. . . . 5
class (π β ((Unitβπ€) βͺ
{(0gβπ€)})) |
37 | 29, 8, 36 | crab 3408 |
. . . 4
class {π β (π β ((Unitβπ€) βͺ {(0gβπ€)})) β£ βπ₯ β π βπ¦ β π [(β₯rβπ€) / π](ππ(π₯(.rβπ€)π¦) β (πππ₯ β¨ πππ¦))} |
38 | 4, 7, 37 | csb 3856 |
. . 3
class
β¦(Baseβπ€) / πβ¦{π β (π β ((Unitβπ€) βͺ {(0gβπ€)})) β£ βπ₯ β π βπ¦ β π [(β₯rβπ€) / π](ππ(π₯(.rβπ€)π¦) β (πππ₯ β¨ πππ¦))} |
39 | 2, 3, 38 | cmpt 5189 |
. 2
class (π€ β V β¦
β¦(Baseβπ€) / πβ¦{π β (π β ((Unitβπ€) βͺ {(0gβπ€)})) β£ βπ₯ β π βπ¦ β π [(β₯rβπ€) / π](ππ(π₯(.rβπ€)π¦) β (πππ₯ β¨ πππ¦))}) |
40 | 1, 39 | wceq 1542 |
1
wff RPrime =
(π€ β V β¦
β¦(Baseβπ€) / πβ¦{π β (π β ((Unitβπ€) βͺ {(0gβπ€)})) β£ βπ₯ β π βπ¦ β π [(β₯rβπ€) / π](ππ(π₯(.rβπ€)π¦) β (πππ₯ β¨ πππ¦))}) |