Step | Hyp | Ref
| Expression |
1 | | opabssxp 5725 |
. . . . . . 7
β’
{β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))} β (π Γ
β+) |
2 | | bcthlem.4 |
. . . . . . . . 9
β’ (π β π· β (CMetβπ)) |
3 | | elfvdm 6880 |
. . . . . . . . 9
β’ (π· β (CMetβπ) β π β dom CMet) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
β’ (π β π β dom CMet) |
5 | | reex 11143 |
. . . . . . . . 9
β’ β
β V |
6 | | rpssre 12923 |
. . . . . . . . 9
β’
β+ β β |
7 | 5, 6 | ssexi 5280 |
. . . . . . . 8
β’
β+ β V |
8 | | xpexg 7685 |
. . . . . . . 8
β’ ((π β dom CMet β§
β+ β V) β (π Γ β+) β
V) |
9 | 4, 7, 8 | sylancl 587 |
. . . . . . 7
β’ (π β (π Γ β+) β
V) |
10 | | ssexg 5281 |
. . . . . . 7
β’
(({β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))} β (π Γ β+) β§ (π Γ β+)
β V) β {β¨π₯,
πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))} β V) |
11 | 1, 9, 10 | sylancr 588 |
. . . . . 6
β’ (π β {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))} β V) |
12 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π = π΄ β (1 / π) = (1 / π΄)) |
13 | 12 | breq2d 5118 |
. . . . . . . . . 10
β’ (π = π΄ β (π < (1 / π) β π < (1 / π΄))) |
14 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = π΄ β (πβπ) = (πβπ΄)) |
15 | 14 | difeq2d 4083 |
. . . . . . . . . . 11
β’ (π = π΄ β (((ballβπ·)βπ§) β (πβπ)) = (((ballβπ·)βπ§) β (πβπ΄))) |
16 | 15 | sseq2d 3977 |
. . . . . . . . . 10
β’ (π = π΄ β (((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ)) β ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ΄)))) |
17 | 13, 16 | anbi12d 632 |
. . . . . . . . 9
β’ (π = π΄ β ((π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))) β (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ΄))))) |
18 | 17 | anbi2d 630 |
. . . . . . . 8
β’ (π = π΄ β (((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ)))) β ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ΄)))))) |
19 | 18 | opabbidv 5172 |
. . . . . . 7
β’ (π = π΄ β {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))} = {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ΄))))}) |
20 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π§ = π΅ β ((ballβπ·)βπ§) = ((ballβπ·)βπ΅)) |
21 | 20 | difeq1d 4082 |
. . . . . . . . . . 11
β’ (π§ = π΅ β (((ballβπ·)βπ§) β (πβπ΄)) = (((ballβπ·)βπ΅) β (πβπ΄))) |
22 | 21 | sseq2d 3977 |
. . . . . . . . . 10
β’ (π§ = π΅ β (((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ΄)) β ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄)))) |
23 | 22 | anbi2d 630 |
. . . . . . . . 9
β’ (π§ = π΅ β ((π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ΄))) β (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))) |
24 | 23 | anbi2d 630 |
. . . . . . . 8
β’ (π§ = π΅ β (((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ΄)))) β ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄)))))) |
25 | 24 | opabbidv 5172 |
. . . . . . 7
β’ (π§ = π΅ β {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ΄))))} = {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))}) |
26 | | bcthlem.5 |
. . . . . . 7
β’ πΉ = (π β β, π§ β (π Γ β+) β¦
{β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) |
27 | 19, 25, 26 | ovmpog 7515 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β (π Γ β+) β§
{β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))} β V) β (π΄πΉπ΅) = {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))}) |
28 | 11, 27 | syl3an3 1166 |
. . . . 5
β’ ((π΄ β β β§ π΅ β (π Γ β+) β§ π) β (π΄πΉπ΅) = {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))}) |
29 | 28 | 3expa 1119 |
. . . 4
β’ (((π΄ β β β§ π΅ β (π Γ β+)) β§ π) β (π΄πΉπ΅) = {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))}) |
30 | 29 | ancoms 460 |
. . 3
β’ ((π β§ (π΄ β β β§ π΅ β (π Γ β+))) β
(π΄πΉπ΅) = {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))}) |
31 | 30 | eleq2d 2824 |
. 2
β’ ((π β§ (π΄ β β β§ π΅ β (π Γ β+))) β
(πΆ β (π΄πΉπ΅) β πΆ β {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))})) |
32 | 1 | sseli 3941 |
. . 3
β’ (πΆ β {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))} β πΆ β (π Γ
β+)) |
33 | | simp1 1137 |
. . 3
β’ ((πΆ β (π Γ β+) β§
(2nd βπΆ)
< (1 / π΄) β§
((clsβπ½)β((ballβπ·)βπΆ)) β (((ballβπ·)βπ΅) β (πβπ΄))) β πΆ β (π Γ
β+)) |
34 | | 1st2nd2 7961 |
. . . . . 6
β’ (πΆ β (π Γ β+) β πΆ = β¨(1st
βπΆ), (2nd
βπΆ)β©) |
35 | 34 | eleq1d 2823 |
. . . . 5
β’ (πΆ β (π Γ β+) β (πΆ β {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))} β β¨(1st
βπΆ), (2nd
βπΆ)β© β
{β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))})) |
36 | | fvex 6856 |
. . . . . 6
β’
(1st βπΆ) β V |
37 | | fvex 6856 |
. . . . . 6
β’
(2nd βπΆ) β V |
38 | | eleq1 2826 |
. . . . . . . 8
β’ (π₯ = (1st βπΆ) β (π₯ β π β (1st βπΆ) β π)) |
39 | | eleq1 2826 |
. . . . . . . 8
β’ (π = (2nd βπΆ) β (π β β+ β
(2nd βπΆ)
β β+)) |
40 | 38, 39 | bi2anan9 638 |
. . . . . . 7
β’ ((π₯ = (1st βπΆ) β§ π = (2nd βπΆ)) β ((π₯ β π β§ π β β+) β
((1st βπΆ)
β π β§
(2nd βπΆ)
β β+))) |
41 | | simpr 486 |
. . . . . . . . 9
β’ ((π₯ = (1st βπΆ) β§ π = (2nd βπΆ)) β π = (2nd βπΆ)) |
42 | 41 | breq1d 5116 |
. . . . . . . 8
β’ ((π₯ = (1st βπΆ) β§ π = (2nd βπΆ)) β (π < (1 / π΄) β (2nd βπΆ) < (1 / π΄))) |
43 | | oveq12 7367 |
. . . . . . . . . 10
β’ ((π₯ = (1st βπΆ) β§ π = (2nd βπΆ)) β (π₯(ballβπ·)π) = ((1st βπΆ)(ballβπ·)(2nd βπΆ))) |
44 | 43 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π₯ = (1st βπΆ) β§ π = (2nd βπΆ)) β ((clsβπ½)β(π₯(ballβπ·)π)) = ((clsβπ½)β((1st βπΆ)(ballβπ·)(2nd βπΆ)))) |
45 | 44 | sseq1d 3976 |
. . . . . . . 8
β’ ((π₯ = (1st βπΆ) β§ π = (2nd βπΆ)) β (((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄)) β ((clsβπ½)β((1st βπΆ)(ballβπ·)(2nd βπΆ))) β (((ballβπ·)βπ΅) β (πβπ΄)))) |
46 | 42, 45 | anbi12d 632 |
. . . . . . 7
β’ ((π₯ = (1st βπΆ) β§ π = (2nd βπΆ)) β ((π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))) β ((2nd βπΆ) < (1 / π΄) β§ ((clsβπ½)β((1st βπΆ)(ballβπ·)(2nd βπΆ))) β (((ballβπ·)βπ΅) β (πβπ΄))))) |
47 | 40, 46 | anbi12d 632 |
. . . . . 6
β’ ((π₯ = (1st βπΆ) β§ π = (2nd βπΆ)) β (((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄)))) β (((1st βπΆ) β π β§ (2nd βπΆ) β β+)
β§ ((2nd βπΆ) < (1 / π΄) β§ ((clsβπ½)β((1st βπΆ)(ballβπ·)(2nd βπΆ))) β (((ballβπ·)βπ΅) β (πβπ΄)))))) |
48 | 36, 37, 47 | opelopaba 5494 |
. . . . 5
β’
(β¨(1st βπΆ), (2nd βπΆ)β© β {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))} β (((1st βπΆ) β π β§ (2nd βπΆ) β β+)
β§ ((2nd βπΆ) < (1 / π΄) β§ ((clsβπ½)β((1st βπΆ)(ballβπ·)(2nd βπΆ))) β (((ballβπ·)βπ΅) β (πβπ΄))))) |
49 | 35, 48 | bitrdi 287 |
. . . 4
β’ (πΆ β (π Γ β+) β (πΆ β {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))} β (((1st βπΆ) β π β§ (2nd βπΆ) β β+)
β§ ((2nd βπΆ) < (1 / π΄) β§ ((clsβπ½)β((1st βπΆ)(ballβπ·)(2nd βπΆ))) β (((ballβπ·)βπ΅) β (πβπ΄)))))) |
50 | 34 | eleq1d 2823 |
. . . . . . 7
β’ (πΆ β (π Γ β+) β (πΆ β (π Γ β+) β
β¨(1st βπΆ), (2nd βπΆ)β© β (π Γ
β+))) |
51 | | opelxp 5670 |
. . . . . . 7
β’
(β¨(1st βπΆ), (2nd βπΆ)β© β (π Γ β+) β
((1st βπΆ)
β π β§
(2nd βπΆ)
β β+)) |
52 | 50, 51 | bitr2di 288 |
. . . . . 6
β’ (πΆ β (π Γ β+) β
(((1st βπΆ)
β π β§
(2nd βπΆ)
β β+) β πΆ β (π Γ
β+))) |
53 | | df-ov 7361 |
. . . . . . . . . 10
β’
((1st βπΆ)(ballβπ·)(2nd βπΆ)) = ((ballβπ·)ββ¨(1st βπΆ), (2nd βπΆ)β©) |
54 | 34 | fveq2d 6847 |
. . . . . . . . . 10
β’ (πΆ β (π Γ β+) β
((ballβπ·)βπΆ) = ((ballβπ·)ββ¨(1st
βπΆ), (2nd
βπΆ)β©)) |
55 | 53, 54 | eqtr4id 2796 |
. . . . . . . . 9
β’ (πΆ β (π Γ β+) β
((1st βπΆ)(ballβπ·)(2nd βπΆ)) = ((ballβπ·)βπΆ)) |
56 | 55 | fveq2d 6847 |
. . . . . . . 8
β’ (πΆ β (π Γ β+) β
((clsβπ½)β((1st βπΆ)(ballβπ·)(2nd βπΆ))) = ((clsβπ½)β((ballβπ·)βπΆ))) |
57 | 56 | sseq1d 3976 |
. . . . . . 7
β’ (πΆ β (π Γ β+) β
(((clsβπ½)β((1st βπΆ)(ballβπ·)(2nd βπΆ))) β (((ballβπ·)βπ΅) β (πβπ΄)) β ((clsβπ½)β((ballβπ·)βπΆ)) β (((ballβπ·)βπ΅) β (πβπ΄)))) |
58 | 57 | anbi2d 630 |
. . . . . 6
β’ (πΆ β (π Γ β+) β
(((2nd βπΆ)
< (1 / π΄) β§
((clsβπ½)β((1st βπΆ)(ballβπ·)(2nd βπΆ))) β (((ballβπ·)βπ΅) β (πβπ΄))) β ((2nd βπΆ) < (1 / π΄) β§ ((clsβπ½)β((ballβπ·)βπΆ)) β (((ballβπ·)βπ΅) β (πβπ΄))))) |
59 | 52, 58 | anbi12d 632 |
. . . . 5
β’ (πΆ β (π Γ β+) β
((((1st βπΆ) β π β§ (2nd βπΆ) β β+)
β§ ((2nd βπΆ) < (1 / π΄) β§ ((clsβπ½)β((1st βπΆ)(ballβπ·)(2nd βπΆ))) β (((ballβπ·)βπ΅) β (πβπ΄)))) β (πΆ β (π Γ β+) β§
((2nd βπΆ)
< (1 / π΄) β§
((clsβπ½)β((ballβπ·)βπΆ)) β (((ballβπ·)βπ΅) β (πβπ΄)))))) |
60 | | 3anass 1096 |
. . . . 5
β’ ((πΆ β (π Γ β+) β§
(2nd βπΆ)
< (1 / π΄) β§
((clsβπ½)β((ballβπ·)βπΆ)) β (((ballβπ·)βπ΅) β (πβπ΄))) β (πΆ β (π Γ β+) β§
((2nd βπΆ)
< (1 / π΄) β§
((clsβπ½)β((ballβπ·)βπΆ)) β (((ballβπ·)βπ΅) β (πβπ΄))))) |
61 | 59, 60 | bitr4di 289 |
. . . 4
β’ (πΆ β (π Γ β+) β
((((1st βπΆ) β π β§ (2nd βπΆ) β β+)
β§ ((2nd βπΆ) < (1 / π΄) β§ ((clsβπ½)β((1st βπΆ)(ballβπ·)(2nd βπΆ))) β (((ballβπ·)βπ΅) β (πβπ΄)))) β (πΆ β (π Γ β+) β§
(2nd βπΆ)
< (1 / π΄) β§
((clsβπ½)β((ballβπ·)βπΆ)) β (((ballβπ·)βπ΅) β (πβπ΄))))) |
62 | 49, 61 | bitrd 279 |
. . 3
β’ (πΆ β (π Γ β+) β (πΆ β {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))} β (πΆ β (π Γ β+) β§
(2nd βπΆ)
< (1 / π΄) β§
((clsβπ½)β((ballβπ·)βπΆ)) β (((ballβπ·)βπ΅) β (πβπ΄))))) |
63 | 32, 33, 62 | pm5.21nii 380 |
. 2
β’ (πΆ β {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π΄) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ΅) β (πβπ΄))))} β (πΆ β (π Γ β+) β§
(2nd βπΆ)
< (1 / π΄) β§
((clsβπ½)β((ballβπ·)βπΆ)) β (((ballβπ·)βπ΅) β (πβπ΄)))) |
64 | 31, 63 | bitrdi 287 |
1
β’ ((π β§ (π΄ β β β§ π΅ β (π Γ β+))) β
(πΆ β (π΄πΉπ΅) β (πΆ β (π Γ β+) β§
(2nd βπΆ)
< (1 / π΄) β§
((clsβπ½)β((ballβπ·)βπΆ)) β (((ballβπ·)βπ΅) β (πβπ΄))))) |