Step | Hyp | Ref
| Expression |
1 | | df-co 5640 |
. . 3
β’
((t*recβπ
)
β (t*recβπ
)) =
{β¨π, πβ© β£ βπ(π(t*recβπ
)π β§ π(t*recβπ
)π)} |
2 | | elopab 5482 |
. . . . 5
β’ (π β {β¨π, πβ© β£ βπ(π(t*recβπ
)π β§ π(t*recβπ
)π)} β βπβπ(π = β¨π, πβ© β§ βπ(π(t*recβπ
)π β§ π(t*recβπ
)π))) |
3 | | eqeq1 2741 |
. . . . . . . . . . 11
β’ (π = β¨π, πβ© β (π = β¨π, πβ© β β¨π, πβ© = β¨π, πβ©)) |
4 | 3 | anbi1d 630 |
. . . . . . . . . 10
β’ (π = β¨π, πβ© β ((π = β¨π, πβ© β§ (βπ(π(t*recβπ
)π β§ π(t*recβπ
)π) β§ π)) β (β¨π, πβ© = β¨π, πβ© β§ (βπ(π(t*recβπ
)π β§ π(t*recβπ
)π) β§ π)))) |
5 | | simprr 771 |
. . . . . . . . . . . 12
β’
((β¨π, πβ© = β¨π, πβ© β§ (βπ(π(t*recβπ
)π β§ π(t*recβπ
)π) β§ π)) β π) |
6 | | simprl 769 |
. . . . . . . . . . . 12
β’
((β¨π, πβ© = β¨π, πβ© β§ (βπ(π(t*recβπ
)π β§ π(t*recβπ
)π) β§ π)) β βπ(π(t*recβπ
)π β§ π(t*recβπ
)π)) |
7 | | simpl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ π)) β π(t*recβπ
)π) |
8 | | simprr 771 |
. . . . . . . . . . . . . . . . . 18
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ π)) β π) |
9 | | rtrclreclem.1 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Rel π
) |
10 | 9 | dfrtrclrec2 14903 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π(t*recβπ
)π β βπ β β0 π(π
βππ)π)) |
11 | 8, 10 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ π)) β (π(t*recβπ
)π β βπ β β0 π(π
βππ)π)) |
12 | 7, 11 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ π)) β βπ β β0 π(π
βππ)π) |
13 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ π β β0)))) β π(t*recβπ
)π) |
14 | | simprrl 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ π β β0)))) β π) |
15 | 9 | dfrtrclrec2 14903 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (π(t*recβπ
)π β βπ β β0 π(π
βππ)π)) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ π β β0)))) β (π(t*recβπ
)π β βπ β β0 π(π
βππ)π)) |
17 | 13, 16 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ π β β0)))) β
βπ β
β0 π(π
βππ)π) |
18 | | simprrl 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))) β π β
β0) |
19 | 18 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))) β π β
β0) |
20 | 19 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))))) β
π β
β0) |
21 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π β β0
β§ (π(π
βππ)π β§ π β β0)) β π β
β0) |
22 | 21 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))) β π β
β0) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))) β π β
β0) |
24 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))) β π β
β0) |
25 | 24 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))))) β
π β
β0) |
26 | 20, 25 | nn0addcld 12435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))))) β
(π + π) β
β0) |
27 | 20 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
π β
β0) |
28 | 27 | nn0cnd 12433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
π β
β) |
29 | 25 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
π β
β0) |
30 | 29 | nn0cnd 12433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
π β
β) |
31 | 28, 30 | addcomd 11315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
(π + π) = (π + π)) |
32 | | eleq1 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π + π) = (π + π) β ((π + π) β β0 β (π + π) β
β0)) |
33 | 32 | anbi1d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π + π) = (π + π) β (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β
β0))))))))) |
34 | | simprrl 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))))) β
π) |
35 | 34 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
π) |
36 | 35, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β Rel
π
) |
37 | 25 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
π β
β0) |
38 | 20 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
π β
β0) |
39 | 36, 37, 38 | relexpaddd 14899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
((π
βππ) β (π
βππ)) = (π
βπ(π + π))) |
40 | | oveq2 7359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((π + π) = (π + π) β (π
βπ(π + π)) = (π
βπ(π + π))) |
41 | 40 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π + π) = (π + π) β (((π
βππ) β (π
βππ)) = (π
βπ(π + π)) β ((π
βππ) β (π
βππ)) = (π
βπ(π + π)))) |
42 | 39, 41 | syl5ibr 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π + π) = (π + π) β (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
((π
βππ) β (π
βππ)) = (π
βπ(π + π)))) |
43 | 33, 42 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π + π) = (π + π) β (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
((π
βππ) β (π
βππ)) = (π
βπ(π + π)))) |
44 | 31, 43 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
((π
βππ) β (π
βππ)) = (π
βπ(π + π))) |
45 | | simprrl 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))) β π(π
βππ)π) |
46 | 45 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))))) β
π(π
βππ)π) |
47 | | simprrl 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ ((π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))) β π(π
βππ)π) |
48 | 47 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ ((π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))) β π(π
βππ)π) |
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))) β π(π
βππ)π) |
50 | 49 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))))) β
π(π
βππ)π) |
51 | 50 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
π(π
βππ)π) |
52 | | vex 3447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ π β V |
53 | | breq2 5107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (β = π β (π(π
βππ)β β π(π
βππ)π)) |
54 | | breq1 5106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (β = π β (β(π
βππ)π β π(π
βππ)π)) |
55 | 53, 54 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (β = π β ((π(π
βππ)β β§ β(π
βππ)π) β (π(π
βππ)π β§ π(π
βππ)π))) |
56 | 52, 55 | spcev 3563 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π(π
βππ)π β§ π(π
βππ)π) β ββ(π(π
βππ)β β§ β(π
βππ)π)) |
57 | 46, 51, 56 | syl2an2 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
ββ(π(π
βππ)β β§ β(π
βππ)π)) |
58 | | vex 3447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ π β V |
59 | | vex 3447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ π β V |
60 | 58, 59 | brco 5824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (π((π
βππ) β (π
βππ))π β ββ(π(π
βππ)β β§ β(π
βππ)π)) |
61 | 57, 60 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
π((π
βππ) β (π
βππ))π) |
62 | 44, 61 | breqdi 5118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
π(π
βπ(π + π))π) |
63 | | oveq2 7359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (π = (π + π) β (π
βππ) = (π
βπ(π + π))) |
64 | 63 | breqd 5114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π = (π + π) β (π(π
βππ)π β π(π
βπ(π + π))π)) |
65 | 64 | rspcev 3579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (((π + π) β β0 β§ π(π
βπ(π + π))π) β βπ β β0 π(π
βππ)π) |
66 | 62, 65 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (((π + π) β β0 β§ (π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))))) β
βπ β
β0 π(π
βππ)π) |
67 | 26, 66 | mpancom 686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))))) β
βπ β
β0 π(π
βππ)π) |
68 | | df-br 5104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π(t*recβπ
)π β β¨π, πβ© β (t*recβπ
)) |
69 | 34, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))))) β Rel
π
) |
70 | 69 | dfrtrclrec2 14903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))))) β
(π(t*recβπ
)π β βπ β β0 π(π
βππ)π)) |
71 | 68, 70 | bitr3id 284 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))))) β
(β¨π, πβ© β (t*recβπ
) β βπ β β0
π(π
βππ)π)) |
72 | 67, 71 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))))) β
β¨π, πβ© β (t*recβπ
)) |
73 | 72 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))))) β
(π(t*recβπ
)π β β¨π, πβ© β (t*recβπ
))) |
74 | 73 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β§ (π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0)))) β (π(t*recβπ
)π β (π(t*recβπ
)π β β¨π, πβ© β (t*recβπ
)))) |
75 | 74 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π(π
βππ)π β§ (π β β0 β§ (π(π
βππ)π β§ π β β0))) β (π β (π(t*recβπ
)π β (π(t*recβπ
)π β β¨π, πβ© β (t*recβπ
))))) |
76 | 75 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π(π
βππ)π β§ π β β0) β§ (π(π
βππ)π β§ π β β0)) β (π β (π(t*recβπ
)π β (π(t*recβπ
)π β β¨π, πβ© β (t*recβπ
))))) |
77 | 76 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ ((π(π
βππ)π β§ π β β0) β§ (π(π
βππ)π β§ π β β0))) β (π(t*recβπ
)π β (π(t*recβπ
)π β β¨π, πβ© β (t*recβπ
)))) |
78 | 77 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ (π(π
βππ)π β§ π β β0)) β§ (π(π
βππ)π β§ π β β0)) β (π(t*recβπ
)π β (π(t*recβπ
)π β β¨π, πβ© β (t*recβπ
)))) |
79 | 78 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π(t*recβπ
)π β§ ((π β§ (π(π
βππ)π β§ π β β0)) β§ (π(π
βππ)π β§ π β β0))) β (π(t*recβπ
)π β β¨π, πβ© β (t*recβπ
))) |
80 | 79 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ π β β0))) β§ (π(π
βππ)π β§ π β β0)) β (π(t*recβπ
)π β β¨π, πβ© β (t*recβπ
))) |
81 | 80 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π(t*recβπ
)π β§ ((π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ π β β0))) β§ (π(π
βππ)π β§ π β β0))) β
β¨π, πβ© β (t*recβπ
)) |
82 | 81 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ π β β0)))) β§ (π(π
βππ)π β§ π β β0)) β
β¨π, πβ© β (t*recβπ
)) |
83 | 82 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π(π
βππ)π β§ π β β0) β ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ π β β0)))) β
β¨π, πβ© β (t*recβπ
))) |
84 | 83 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β0
β (π(π
βππ)π β ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ π β β0)))) β
β¨π, πβ© β (t*recβπ
)))) |
85 | 84 | rexlimiv 3143 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ β
β0 π(π
βππ)π β ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ π β β0)))) β
β¨π, πβ© β (t*recβπ
))) |
86 | 17, 85 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ π β β0)))) β
β¨π, πβ© β (t*recβπ
)) |
87 | 86 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π(t*recβπ
)π β§ (π β§ (π(π
βππ)π β§ π β β0))) β (π(t*recβπ
)π β β¨π, πβ© β (t*recβπ
))) |
88 | 87 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π(t*recβπ
)π β§ π) β§ (π(π
βππ)π β§ π β β0)) β (π(t*recβπ
)π β β¨π, πβ© β (t*recβπ
))) |
89 | 88 | impcom 408 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π(t*recβπ
)π β§ ((π(t*recβπ
)π β§ π) β§ (π(π
βππ)π β§ π β β0))) β
β¨π, πβ© β (t*recβπ
)) |
90 | 89 | anassrs 468 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ π)) β§ (π(π
βππ)π β§ π β β0)) β
β¨π, πβ© β (t*recβπ
)) |
91 | 90 | expcom 414 |
. . . . . . . . . . . . . . . . . 18
β’ ((π(π
βππ)π β§ π β β0) β ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ π)) β β¨π, πβ© β (t*recβπ
))) |
92 | 91 | expcom 414 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (π(π
βππ)π β ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ π)) β β¨π, πβ© β (t*recβπ
)))) |
93 | 92 | rexlimiv 3143 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
β0 π(π
βππ)π β ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ π)) β β¨π, πβ© β (t*recβπ
))) |
94 | 12, 93 | mpcom 38 |
. . . . . . . . . . . . . . 15
β’ ((π(t*recβπ
)π β§ (π(t*recβπ
)π β§ π)) β β¨π, πβ© β (t*recβπ
)) |
95 | 94 | anassrs 468 |
. . . . . . . . . . . . . 14
β’ (((π(t*recβπ
)π β§ π(t*recβπ
)π) β§ π) β β¨π, πβ© β (t*recβπ
)) |
96 | 95 | expcom 414 |
. . . . . . . . . . . . 13
β’ (π β ((π(t*recβπ
)π β§ π(t*recβπ
)π) β β¨π, πβ© β (t*recβπ
))) |
97 | 96 | exlimdv 1936 |
. . . . . . . . . . . 12
β’ (π β (βπ(π(t*recβπ
)π β§ π(t*recβπ
)π) β β¨π, πβ© β (t*recβπ
))) |
98 | 5, 6, 97 | sylc 65 |
. . . . . . . . . . 11
β’
((β¨π, πβ© = β¨π, πβ© β§ (βπ(π(t*recβπ
)π β§ π(t*recβπ
)π) β§ π)) β β¨π, πβ© β (t*recβπ
)) |
99 | | eleq1 2825 |
. . . . . . . . . . 11
β’ (π = β¨π, πβ© β (π β (t*recβπ
) β β¨π, πβ© β (t*recβπ
))) |
100 | 98, 99 | syl5ibr 245 |
. . . . . . . . . 10
β’ (π = β¨π, πβ© β ((β¨π, πβ© = β¨π, πβ© β§ (βπ(π(t*recβπ
)π β§ π(t*recβπ
)π) β§ π)) β π β (t*recβπ
))) |
101 | 4, 100 | sylbid 239 |
. . . . . . . . 9
β’ (π = β¨π, πβ© β ((π = β¨π, πβ© β§ (βπ(π(t*recβπ
)π β§ π(t*recβπ
)π) β§ π)) β π β (t*recβπ
))) |
102 | 101 | anabsi5 667 |
. . . . . . . 8
β’ ((π = β¨π, πβ© β§ (βπ(π(t*recβπ
)π β§ π(t*recβπ
)π) β§ π)) β π β (t*recβπ
)) |
103 | 102 | anassrs 468 |
. . . . . . 7
β’ (((π = β¨π, πβ© β§ βπ(π(t*recβπ
)π β§ π(t*recβπ
)π)) β§ π) β π β (t*recβπ
)) |
104 | 103 | expcom 414 |
. . . . . 6
β’ (π β ((π = β¨π, πβ© β§ βπ(π(t*recβπ
)π β§ π(t*recβπ
)π)) β π β (t*recβπ
))) |
105 | 104 | exlimdvv 1937 |
. . . . 5
β’ (π β (βπβπ(π = β¨π, πβ© β§ βπ(π(t*recβπ
)π β§ π(t*recβπ
)π)) β π β (t*recβπ
))) |
106 | 2, 105 | biimtrid 241 |
. . . 4
β’ (π β (π β {β¨π, πβ© β£ βπ(π(t*recβπ
)π β§ π(t*recβπ
)π)} β π β (t*recβπ
))) |
107 | | eleq2 2826 |
. . . . 5
β’
(((t*recβπ
)
β (t*recβπ
)) =
{β¨π, πβ© β£ βπ(π(t*recβπ
)π β§ π(t*recβπ
)π)} β (π β ((t*recβπ
) β (t*recβπ
)) β π β {β¨π, πβ© β£ βπ(π(t*recβπ
)π β§ π(t*recβπ
)π)})) |
108 | 107 | imbi1d 341 |
. . . 4
β’
(((t*recβπ
)
β (t*recβπ
)) =
{β¨π, πβ© β£ βπ(π(t*recβπ
)π β§ π(t*recβπ
)π)} β ((π β ((t*recβπ
) β (t*recβπ
)) β π β (t*recβπ
)) β (π β {β¨π, πβ© β£ βπ(π(t*recβπ
)π β§ π(t*recβπ
)π)} β π β (t*recβπ
)))) |
109 | 106, 108 | syl5ibr 245 |
. . 3
β’
(((t*recβπ
)
β (t*recβπ
)) =
{β¨π, πβ© β£ βπ(π(t*recβπ
)π β§ π(t*recβπ
)π)} β (π β (π β ((t*recβπ
) β (t*recβπ
)) β π β (t*recβπ
)))) |
110 | 1, 109 | ax-mp 5 |
. 2
β’ (π β (π β ((t*recβπ
) β (t*recβπ
)) β π β (t*recβπ
))) |
111 | 110 | ssrdv 3948 |
1
β’ (π β ((t*recβπ
) β (t*recβπ
)) β (t*recβπ
)) |