Step | Hyp | Ref
| Expression |
1 | | reeanv 3216 |
. . . . . 6
β’
(βπ β
β βπ β
β (((π β
(πΌβπ) β§
π β
(πΌβπ) β§
π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β§ ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})) β (βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β§ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}))) |
2 | | simp1 1137 |
. . . . . . . . . . 11
β’ ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β π β (πΌβπ)) |
3 | | simp1 1137 |
. . . . . . . . . . 11
β’ ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β π β (πΌβπ)) |
4 | | axdimuniq 27911 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β (πΌβπ)) β§ (π β β β§ π β (πΌβπ))) β π = π) |
5 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (πΌβπ) = (πΌβπ)) |
6 | | rabeq 3420 |
. . . . . . . . . . . . . . . . . . 19
β’
((πΌβπ)
= (πΌβπ) β
{π₯ β
(πΌβπ) β£
πOutsideOfβ¨π, π₯β©} = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) |
8 | 7 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})) |
9 | 8 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β (π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}))) |
10 | | eqtr3 2759 |
. . . . . . . . . . . . . . . 16
β’ ((π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β π = π ) |
11 | 9, 10 | syl6bi 253 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β π = π )) |
12 | 4, 11 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β (πΌβπ)) β§ (π β β β§ π β (πΌβπ))) β ((π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β π = π )) |
13 | 12 | an4s 659 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β) β§ (π β (πΌβπ) β§ π β (πΌβπ))) β ((π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β π = π )) |
14 | 13 | ex 414 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β) β ((π β (πΌβπ) β§ π β (πΌβπ)) β ((π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β π = π ))) |
15 | 14 | com3l 89 |
. . . . . . . . . . 11
β’ ((π β (πΌβπ) β§ π β (πΌβπ)) β ((π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β ((π β β β§ π β β) β π = π ))) |
16 | 2, 3, 15 | syl2an 597 |
. . . . . . . . . 10
β’ (((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β ((π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β ((π β β β§ π β β) β π = π ))) |
17 | 16 | imp 408 |
. . . . . . . . 9
β’ ((((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β§ (π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})) β ((π β β β§ π β β) β π = π )) |
18 | 17 | an4s 659 |
. . . . . . . 8
β’ ((((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β§ ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})) β ((π β β β§ π β β) β π = π )) |
19 | 18 | com12 32 |
. . . . . . 7
β’ ((π β β β§ π β β) β
((((π β
(πΌβπ) β§
π β
(πΌβπ) β§
π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β§ ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})) β π = π )) |
20 | 19 | rexlimivv 3193 |
. . . . . 6
β’
(βπ β
β βπ β
β (((π β
(πΌβπ) β§
π β
(πΌβπ) β§
π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β§ ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})) β π = π ) |
21 | 1, 20 | sylbir 234 |
. . . . 5
β’
((βπ β
β ((π β
(πΌβπ) β§
π β
(πΌβπ) β§
π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β§ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})) β π = π ) |
22 | 21 | gen2 1799 |
. . . 4
β’
βπβπ ((βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β§ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})) β π = π ) |
23 | | eqeq1 2737 |
. . . . . . . 8
β’ (π = π β (π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})) |
24 | 23 | anbi2d 630 |
. . . . . . 7
β’ (π = π β (((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}))) |
25 | 24 | rexbidv 3172 |
. . . . . 6
β’ (π = π β (βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}))) |
26 | 5 | eleq2d 2820 |
. . . . . . . . 9
β’ (π = π β (π β (πΌβπ) β π β (πΌβπ))) |
27 | 5 | eleq2d 2820 |
. . . . . . . . 9
β’ (π = π β (π β (πΌβπ) β π β (πΌβπ))) |
28 | 26, 27 | 3anbi12d 1438 |
. . . . . . . 8
β’ (π = π β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π))) |
29 | 7 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = π β (π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} β π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})) |
30 | 28, 29 | anbi12d 632 |
. . . . . . 7
β’ (π = π β (((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}))) |
31 | 30 | cbvrexvw 3225 |
. . . . . 6
β’
(βπ β
β ((π β
(πΌβπ) β§
π β
(πΌβπ) β§
π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})) |
32 | 25, 31 | bitrdi 287 |
. . . . 5
β’ (π = π β (βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}))) |
33 | 32 | mo4 2561 |
. . . 4
β’
(β*πβπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β βπβπ ((βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) β§ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})) β π = π )) |
34 | 22, 33 | mpbir 230 |
. . 3
β’
β*πβπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) |
35 | 34 | funoprab 7482 |
. 2
β’ Fun
{β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})} |
36 | | df-ray 34776 |
. . 3
β’ Ray =
{β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})} |
37 | 36 | funeqi 6526 |
. 2
β’ (Fun Ray
β Fun {β¨β¨π,
πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})}) |
38 | 35, 37 | mpbir 230 |
1
β’ Fun
Ray |