Step | Hyp | Ref
| Expression |
1 | | methaus.1 |
. . . . 5
β’ π½ = (MetOpenβπ·) |
2 | 1 | mopntop 23809 |
. . . 4
β’ (π· β (βMetβπ) β π½ β Top) |
3 | 2 | adantr 482 |
. . 3
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β π½ β Top) |
4 | | simpll 766 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π₯ β β β§ π¦ β π΄)) β π· β (βMetβπ)) |
5 | | simplr1 1216 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π₯ β β β§ π¦ β π΄)) β π΄ β π) |
6 | | simprr 772 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π₯ β β β§ π¦ β π΄)) β π¦ β π΄) |
7 | 5, 6 | sseldd 3946 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π₯ β β β§ π¦ β π΄)) β π¦ β π) |
8 | | simprl 770 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π₯ β β β§ π¦ β π΄)) β π₯ β β) |
9 | 8 | nnrpd 12960 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π₯ β β β§ π¦ β π΄)) β π₯ β β+) |
10 | 9 | rpreccld 12972 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π₯ β β β§ π¦ β π΄)) β (1 / π₯) β
β+) |
11 | 10 | rpxrd 12963 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π₯ β β β§ π¦ β π΄)) β (1 / π₯) β
β*) |
12 | 1 | blopn 23872 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π¦ β π β§ (1 / π₯) β β*) β (π¦(ballβπ·)(1 / π₯)) β π½) |
13 | 4, 7, 11, 12 | syl3anc 1372 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π₯ β β β§ π¦ β π΄)) β (π¦(ballβπ·)(1 / π₯)) β π½) |
14 | 13 | ralrimivva 3194 |
. . . . 5
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β βπ₯ β β βπ¦ β π΄ (π¦(ballβπ·)(1 / π₯)) β π½) |
15 | | eqid 2733 |
. . . . . 6
β’ (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) = (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) |
16 | 15 | fmpo 8001 |
. . . . 5
β’
(βπ₯ β
β βπ¦ β
π΄ (π¦(ballβπ·)(1 / π₯)) β π½ β (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))):(β Γ π΄)βΆπ½) |
17 | 14, 16 | sylib 217 |
. . . 4
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))):(β Γ π΄)βΆπ½) |
18 | 17 | frnd 6677 |
. . 3
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) β π½) |
19 | | simpll 766 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β π· β (βMetβπ)) |
20 | | simprl 770 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β π’ β π½) |
21 | | simprr 772 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β π§ β π’) |
22 | 1 | mopni2 23865 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π’ β π½ β§ π§ β π’) β βπ β β+ (π§(ballβπ·)π) β π’) |
23 | 19, 20, 21, 22 | syl3anc 1372 |
. . . . 5
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β βπ β β+ (π§(ballβπ·)π) β π’) |
24 | | simprl 770 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ (π β β+ β§ (π§(ballβπ·)π) β π’)) β π β β+) |
25 | 24 | rphalfcld 12974 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ (π β β+ β§ (π§(ballβπ·)π) β π’)) β (π / 2) β
β+) |
26 | | elrp 12922 |
. . . . . . . 8
β’ ((π / 2) β β+
β ((π / 2) β
β β§ 0 < (π /
2))) |
27 | | nnrecl 12416 |
. . . . . . . 8
β’ (((π / 2) β β β§ 0
< (π / 2)) β
βπ β β (1
/ π) < (π / 2)) |
28 | 26, 27 | sylbi 216 |
. . . . . . 7
β’ ((π / 2) β β+
β βπ β
β (1 / π) < (π / 2)) |
29 | 25, 28 | syl 17 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ (π β β+ β§ (π§(ballβπ·)π) β π’)) β βπ β β (1 / π) < (π / 2)) |
30 | 3 | ad2antrr 725 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π½ β Top) |
31 | | simpr1 1195 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β π΄ β π) |
32 | 31 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π΄ β π) |
33 | 1 | mopnuni 23810 |
. . . . . . . . . . . 12
β’ (π· β (βMetβπ) β π = βͺ π½) |
34 | 33 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π = βͺ π½) |
35 | 32, 34 | sseqtrd 3985 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π΄ β βͺ π½) |
36 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π§ β π’) |
37 | | simplrl 776 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π’ β π½) |
38 | | elunii 4871 |
. . . . . . . . . . . . 13
β’ ((π§ β π’ β§ π’ β π½) β π§ β βͺ π½) |
39 | 36, 37, 38 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π§ β βͺ π½) |
40 | 39, 34 | eleqtrrd 2837 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π§ β π) |
41 | | simpr3 1197 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β ((clsβπ½)βπ΄) = π) |
42 | 41 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β ((clsβπ½)βπ΄) = π) |
43 | 40, 42 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π§ β ((clsβπ½)βπ΄)) |
44 | 19 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π· β (βMetβπ)) |
45 | | simprrl 780 |
. . . . . . . . . . . . . 14
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π β β) |
46 | 45 | nnrpd 12960 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π β β+) |
47 | 46 | rpreccld 12972 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β (1 / π) β
β+) |
48 | 47 | rpxrd 12963 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β (1 / π) β
β*) |
49 | 1 | blopn 23872 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π§ β π β§ (1 / π) β β*) β (π§(ballβπ·)(1 / π)) β π½) |
50 | 44, 40, 48, 49 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β (π§(ballβπ·)(1 / π)) β π½) |
51 | | blcntr 23782 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π§ β π β§ (1 / π) β β+) β π§ β (π§(ballβπ·)(1 / π))) |
52 | 44, 40, 47, 51 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π§ β (π§(ballβπ·)(1 / π))) |
53 | | eqid 2733 |
. . . . . . . . . . 11
β’ βͺ π½ =
βͺ π½ |
54 | 53 | clsndisj 22442 |
. . . . . . . . . 10
β’ (((π½ β Top β§ π΄ β βͺ π½
β§ π§ β
((clsβπ½)βπ΄)) β§ ((π§(ballβπ·)(1 / π)) β π½ β§ π§ β (π§(ballβπ·)(1 / π)))) β ((π§(ballβπ·)(1 / π)) β© π΄) β β
) |
55 | 30, 35, 43, 50, 52, 54 | syl32anc 1379 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β ((π§(ballβπ·)(1 / π)) β© π΄) β β
) |
56 | | n0 4307 |
. . . . . . . . 9
β’ (((π§(ballβπ·)(1 / π)) β© π΄) β β
β βπ‘ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) |
57 | 55, 56 | sylib 217 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β βπ‘ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) |
58 | 45 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β π β β) |
59 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) |
60 | 59 | elin2d 4160 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β π‘ β π΄) |
61 | | eqidd 2734 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β (π‘(ballβπ·)(1 / π)) = (π‘(ballβπ·)(1 / π))) |
62 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (1 / π₯) = (1 / π)) |
63 | 62 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (π¦(ballβπ·)(1 / π₯)) = (π¦(ballβπ·)(1 / π))) |
64 | 63 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π₯ = π β ((π‘(ballβπ·)(1 / π)) = (π¦(ballβπ·)(1 / π₯)) β (π‘(ballβπ·)(1 / π)) = (π¦(ballβπ·)(1 / π)))) |
65 | | oveq1 7365 |
. . . . . . . . . . . . 13
β’ (π¦ = π‘ β (π¦(ballβπ·)(1 / π)) = (π‘(ballβπ·)(1 / π))) |
66 | 65 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π¦ = π‘ β ((π‘(ballβπ·)(1 / π)) = (π¦(ballβπ·)(1 / π)) β (π‘(ballβπ·)(1 / π)) = (π‘(ballβπ·)(1 / π)))) |
67 | 64, 66 | rspc2ev 3591 |
. . . . . . . . . . 11
β’ ((π β β β§ π‘ β π΄ β§ (π‘(ballβπ·)(1 / π)) = (π‘(ballβπ·)(1 / π))) β βπ₯ β β βπ¦ β π΄ (π‘(ballβπ·)(1 / π)) = (π¦(ballβπ·)(1 / π₯))) |
68 | 58, 60, 61, 67 | syl3anc 1372 |
. . . . . . . . . 10
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β βπ₯ β β βπ¦ β π΄ (π‘(ballβπ·)(1 / π)) = (π¦(ballβπ·)(1 / π₯))) |
69 | | ovex 7391 |
. . . . . . . . . . 11
β’ (π‘(ballβπ·)(1 / π)) β V |
70 | | eqeq1 2737 |
. . . . . . . . . . . 12
β’ (π§ = (π‘(ballβπ·)(1 / π)) β (π§ = (π¦(ballβπ·)(1 / π₯)) β (π‘(ballβπ·)(1 / π)) = (π¦(ballβπ·)(1 / π₯)))) |
71 | 70 | 2rexbidv 3210 |
. . . . . . . . . . 11
β’ (π§ = (π‘(ballβπ·)(1 / π)) β (βπ₯ β β βπ¦ β π΄ π§ = (π¦(ballβπ·)(1 / π₯)) β βπ₯ β β βπ¦ β π΄ (π‘(ballβπ·)(1 / π)) = (π¦(ballβπ·)(1 / π₯)))) |
72 | 15 | rnmpo 7490 |
. . . . . . . . . . 11
β’ ran
(π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) = {π§ β£ βπ₯ β β βπ¦ β π΄ π§ = (π¦(ballβπ·)(1 / π₯))} |
73 | 69, 71, 72 | elab2 3635 |
. . . . . . . . . 10
β’ ((π‘(ballβπ·)(1 / π)) β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) β βπ₯ β β βπ¦ β π΄ (π‘(ballβπ·)(1 / π)) = (π¦(ballβπ·)(1 / π₯))) |
74 | 68, 73 | sylibr 233 |
. . . . . . . . 9
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β (π‘(ballβπ·)(1 / π)) β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))) |
75 | 59 | elin1d 4159 |
. . . . . . . . . 10
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β π‘ β (π§(ballβπ·)(1 / π))) |
76 | 44 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β π· β (βMetβπ)) |
77 | 48 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β (1 / π) β
β*) |
78 | 40 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β π§ β π) |
79 | 32 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β π΄ β π) |
80 | 79, 60 | sseldd 3946 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β π‘ β π) |
81 | | blcom 23763 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ (1 / π) β β*) β§ (π§ β π β§ π‘ β π)) β (π‘ β (π§(ballβπ·)(1 / π)) β π§ β (π‘(ballβπ·)(1 / π)))) |
82 | 76, 77, 78, 80, 81 | syl22anc 838 |
. . . . . . . . . 10
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β (π‘ β (π§(ballβπ·)(1 / π)) β π§ β (π‘(ballβπ·)(1 / π)))) |
83 | 75, 82 | mpbid 231 |
. . . . . . . . 9
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β π§ β (π‘(ballβπ·)(1 / π))) |
84 | | simprll 778 |
. . . . . . . . . . . . . 14
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β π β β+) |
85 | 84 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β π β β+) |
86 | 85 | rphalfcld 12974 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β (π / 2) β
β+) |
87 | 86 | rpxrd 12963 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β (π / 2) β
β*) |
88 | | simprrr 781 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β (1 / π) < (π / 2)) |
89 | 84 | rphalfcld 12974 |
. . . . . . . . . . . . . 14
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β (π / 2) β
β+) |
90 | | rpre 12928 |
. . . . . . . . . . . . . . 15
β’ ((1 /
π) β
β+ β (1 / π) β β) |
91 | | rpre 12928 |
. . . . . . . . . . . . . . 15
β’ ((π / 2) β β+
β (π / 2) β
β) |
92 | | ltle 11248 |
. . . . . . . . . . . . . . 15
β’ (((1 /
π) β β β§
(π / 2) β β)
β ((1 / π) < (π / 2) β (1 / π) β€ (π / 2))) |
93 | 90, 91, 92 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((1 /
π) β
β+ β§ (π / 2) β β+) β ((1
/ π) < (π / 2) β (1 / π) β€ (π / 2))) |
94 | 47, 89, 93 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β ((1 / π) < (π / 2) β (1 / π) β€ (π / 2))) |
95 | 88, 94 | mpd 15 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β (1 / π) β€ (π / 2)) |
96 | 95 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β (1 / π) β€ (π / 2)) |
97 | | ssbl 23792 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π‘ β π) β§ ((1 / π) β β* β§ (π / 2) β
β*) β§ (1 / π) β€ (π / 2)) β (π‘(ballβπ·)(1 / π)) β (π‘(ballβπ·)(π / 2))) |
98 | 76, 80, 77, 87, 96, 97 | syl221anc 1382 |
. . . . . . . . . 10
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β (π‘(ballβπ·)(1 / π)) β (π‘(ballβπ·)(π / 2))) |
99 | 85 | rpred 12962 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β π β β) |
100 | 98, 83 | sseldd 3946 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β π§ β (π‘(ballβπ·)(π / 2))) |
101 | | blhalf 23774 |
. . . . . . . . . . . 12
β’ (((π· β (βMetβπ) β§ π‘ β π) β§ (π β β β§ π§ β (π‘(ballβπ·)(π / 2)))) β (π‘(ballβπ·)(π / 2)) β (π§(ballβπ·)π)) |
102 | 76, 80, 99, 100, 101 | syl22anc 838 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β (π‘(ballβπ·)(π / 2)) β (π§(ballβπ·)π)) |
103 | | simprlr 779 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β (π§(ballβπ·)π) β π’) |
104 | 103 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β (π§(ballβπ·)π) β π’) |
105 | 102, 104 | sstrd 3955 |
. . . . . . . . . 10
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β (π‘(ballβπ·)(π / 2)) β π’) |
106 | 98, 105 | sstrd 3955 |
. . . . . . . . 9
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β (π‘(ballβπ·)(1 / π)) β π’) |
107 | | eleq2 2823 |
. . . . . . . . . . 11
β’ (π€ = (π‘(ballβπ·)(1 / π)) β (π§ β π€ β π§ β (π‘(ballβπ·)(1 / π)))) |
108 | | sseq1 3970 |
. . . . . . . . . . 11
β’ (π€ = (π‘(ballβπ·)(1 / π)) β (π€ β π’ β (π‘(ballβπ·)(1 / π)) β π’)) |
109 | 107, 108 | anbi12d 632 |
. . . . . . . . . 10
β’ (π€ = (π‘(ballβπ·)(1 / π)) β ((π§ β π€ β§ π€ β π’) β (π§ β (π‘(ballβπ·)(1 / π)) β§ (π‘(ballβπ·)(1 / π)) β π’))) |
110 | 109 | rspcev 3580 |
. . . . . . . . 9
β’ (((π‘(ballβπ·)(1 / π)) β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) β§ (π§ β (π‘(ballβπ·)(1 / π)) β§ (π‘(ballβπ·)(1 / π)) β π’)) β βπ€ β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))(π§ β π€ β§ π€ β π’)) |
111 | 74, 83, 106, 110 | syl12anc 836 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β§ π‘ β ((π§(ballβπ·)(1 / π)) β© π΄)) β βπ€ β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))(π§ β π€ β§ π€ β π’)) |
112 | 57, 111 | exlimddv 1939 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ ((π β β+ β§ (π§(ballβπ·)π) β π’) β§ (π β β β§ (1 / π) < (π / 2)))) β βπ€ β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))(π§ β π€ β§ π€ β π’)) |
113 | 112 | anassrs 469 |
. . . . . 6
β’
(((((π· β
(βMetβπ) β§
(π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ (π β β+ β§ (π§(ballβπ·)π) β π’)) β§ (π β β β§ (1 / π) < (π / 2))) β βπ€ β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))(π§ β π€ β§ π€ β π’)) |
114 | 29, 113 | rexlimddv 3155 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β§ (π β β+ β§ (π§(ballβπ·)π) β π’)) β βπ€ β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))(π§ β π€ β§ π€ β π’)) |
115 | 23, 114 | rexlimddv 3155 |
. . . 4
β’ (((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β§ (π’ β π½ β§ π§ β π’)) β βπ€ β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))(π§ β π€ β§ π€ β π’)) |
116 | 115 | ralrimivva 3194 |
. . 3
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β βπ’ β π½ βπ§ β π’ βπ€ β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))(π§ β π€ β§ π€ β π’)) |
117 | | basgen2 22355 |
. . 3
β’ ((π½ β Top β§ ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) β π½ β§ βπ’ β π½ βπ§ β π’ βπ€ β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))(π§ β π€ β§ π€ β π’)) β (topGenβran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))) = π½) |
118 | 3, 18, 116, 117 | syl3anc 1372 |
. 2
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β (topGenβran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))) = π½) |
119 | 118, 3 | eqeltrd 2834 |
. . . 4
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β (topGenβran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))) β Top) |
120 | | tgclb 22336 |
. . . 4
β’ (ran
(π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) β TopBases β (topGenβran
(π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))) β Top) |
121 | 119, 120 | sylibr 233 |
. . 3
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) β TopBases) |
122 | | omelon 9587 |
. . . . . 6
β’ Ο
β On |
123 | | simpr2 1196 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β π΄ βΌ Ο) |
124 | | nnex 12164 |
. . . . . . . . 9
β’ β
β V |
125 | 124 | xpdom2 9014 |
. . . . . . . 8
β’ (π΄ βΌ Ο β (β
Γ π΄) βΌ (β
Γ Ο)) |
126 | 123, 125 | syl 17 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β (β Γ π΄) βΌ (β Γ
Ο)) |
127 | | nnenom 13891 |
. . . . . . . . 9
β’ β
β Ο |
128 | | omex 9584 |
. . . . . . . . . 10
β’ Ο
β V |
129 | 128 | enref 8928 |
. . . . . . . . 9
β’ Ο
β Ο |
130 | | xpen 9087 |
. . . . . . . . 9
β’ ((β
β Ο β§ Ο β Ο) β (β Γ Ο)
β (Ο Γ Ο)) |
131 | 127, 129,
130 | mp2an 691 |
. . . . . . . 8
β’ (β
Γ Ο) β (Ο Γ Ο) |
132 | | xpomen 9956 |
. . . . . . . 8
β’ (Ο
Γ Ο) β Ο |
133 | 131, 132 | entri 8951 |
. . . . . . 7
β’ (β
Γ Ο) β Ο |
134 | | domentr 8956 |
. . . . . . 7
β’
(((β Γ π΄) βΌ (β Γ Ο) β§
(β Γ Ο) β Ο) β (β Γ π΄) βΌ
Ο) |
135 | 126, 133,
134 | sylancl 587 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β (β Γ π΄) βΌ Ο) |
136 | | ondomen 9978 |
. . . . . 6
β’ ((Ο
β On β§ (β Γ π΄) βΌ Ο) β (β Γ
π΄) β dom
card) |
137 | 122, 135,
136 | sylancr 588 |
. . . . 5
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β (β Γ π΄) β dom card) |
138 | 17 | ffnd 6670 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) Fn (β Γ π΄)) |
139 | | dffn4 6763 |
. . . . . 6
β’ ((π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) Fn (β Γ π΄) β (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))):(β Γ π΄)βontoβran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))) |
140 | 138, 139 | sylib 217 |
. . . . 5
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))):(β Γ π΄)βontoβran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))) |
141 | | fodomnum 9998 |
. . . . 5
β’ ((β
Γ π΄) β dom card
β ((π₯ β β,
π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))):(β Γ π΄)βontoβran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) βΌ (β Γ π΄))) |
142 | 137, 140,
141 | sylc 65 |
. . . 4
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) βΌ (β Γ π΄)) |
143 | | domtr 8950 |
. . . 4
β’ ((ran
(π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) βΌ (β Γ π΄) β§ (β Γ π΄) βΌ Ο) β ran
(π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) βΌ Ο) |
144 | 142, 135,
143 | syl2anc 585 |
. . 3
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) βΌ Ο) |
145 | | 2ndci 22815 |
. . 3
β’ ((ran
(π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) β TopBases β§ ran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯))) βΌ Ο) β (topGenβran
(π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))) β
2ndΟ) |
146 | 121, 144,
145 | syl2anc 585 |
. 2
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β (topGenβran (π₯ β β, π¦ β π΄ β¦ (π¦(ballβπ·)(1 / π₯)))) β
2ndΟ) |
147 | 118, 146 | eqeltrrd 2835 |
1
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΄ βΌ Ο β§ ((clsβπ½)βπ΄) = π)) β π½ β
2ndΟ) |