Step | Hyp | Ref
| Expression |
1 | | cray 34773 |
. 2
class
Ray |
2 | | vp |
. . . . . . . 8
setvar π |
3 | 2 | cv 1541 |
. . . . . . 7
class π |
4 | | vn |
. . . . . . . . 9
setvar π |
5 | 4 | cv 1541 |
. . . . . . . 8
class π |
6 | | cee 27886 |
. . . . . . . 8
class
πΌ |
7 | 5, 6 | cfv 6500 |
. . . . . . 7
class
(πΌβπ) |
8 | 3, 7 | wcel 2107 |
. . . . . 6
wff π β (πΌβπ) |
9 | | va |
. . . . . . . 8
setvar π |
10 | 9 | cv 1541 |
. . . . . . 7
class π |
11 | 10, 7 | wcel 2107 |
. . . . . 6
wff π β (πΌβπ) |
12 | 3, 10 | wne 2940 |
. . . . . 6
wff π β π |
13 | 8, 11, 12 | w3a 1088 |
. . . . 5
wff (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) |
14 | | vr |
. . . . . . 7
setvar π |
15 | 14 | cv 1541 |
. . . . . 6
class π |
16 | | vx |
. . . . . . . . . 10
setvar π₯ |
17 | 16 | cv 1541 |
. . . . . . . . 9
class π₯ |
18 | 10, 17 | cop 4596 |
. . . . . . . 8
class
β¨π, π₯β© |
19 | | coutsideof 34757 |
. . . . . . . 8
class
OutsideOf |
20 | 3, 18, 19 | wbr 5109 |
. . . . . . 7
wff πOutsideOfβ¨π, π₯β© |
21 | 20, 16, 7 | crab 3406 |
. . . . . 6
class {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} |
22 | 15, 21 | wceq 1542 |
. . . . 5
wff π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} |
23 | 13, 22 | wa 397 |
. . . 4
wff ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) |
24 | | cn 12161 |
. . . 4
class
β |
25 | 23, 4, 24 | wrex 3070 |
. . 3
wff
βπ β
β ((π β
(πΌβπ) β§
π β
(πΌβπ) β§
π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) |
26 | 25, 2, 9, 14 | coprab 7362 |
. 2
class
{β¨β¨π,
πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})} |
27 | 1, 26 | wceq 1542 |
1
wff Ray =
{β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})} |