Step | Hyp | Ref
| Expression |
1 | | methaus.1 |
. . 3
β’ π½ = (MetOpenβπ·) |
2 | 1 | mopntop 23809 |
. 2
β’ (π· β (βMetβπ) β π½ β Top) |
3 | 1 | mopnuni 23810 |
. . . . . 6
β’ (π· β (βMetβπ) β π = βͺ π½) |
4 | 3 | eleq2d 2820 |
. . . . 5
β’ (π· β (βMetβπ) β (π₯ β π β π₯ β βͺ π½)) |
5 | 4 | biimpar 479 |
. . . 4
β’ ((π· β (βMetβπ) β§ π₯ β βͺ π½) β π₯ β π) |
6 | | simpll 766 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ π β β) β π· β (βMetβπ)) |
7 | | simplr 768 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ π β β) β π₯ β π) |
8 | | nnrp 12931 |
. . . . . . . . . . . 12
β’ (π β β β π β
β+) |
9 | 8 | adantl 483 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ π β β) β π β β+) |
10 | 9 | rpreccld 12972 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ π β β) β (1 / π) β
β+) |
11 | 10 | rpxrd 12963 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ π β β) β (1 / π) β
β*) |
12 | 1 | blopn 23872 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π₯ β π β§ (1 / π) β β*) β (π₯(ballβπ·)(1 / π)) β π½) |
13 | 6, 7, 11, 12 | syl3anc 1372 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ π β β) β (π₯(ballβπ·)(1 / π)) β π½) |
14 | 13 | fmpttd 7064 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π₯ β π) β (π β β β¦ (π₯(ballβπ·)(1 / π))):ββΆπ½) |
15 | 14 | frnd 6677 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π₯ β π) β ran (π β β β¦ (π₯(ballβπ·)(1 / π))) β π½) |
16 | | nnex 12164 |
. . . . . . . . 9
β’ β
β V |
17 | 16 | mptex 7174 |
. . . . . . . 8
β’ (π β β β¦ (π₯(ballβπ·)(1 / π))) β V |
18 | 17 | rnex 7850 |
. . . . . . 7
β’ ran
(π β β β¦
(π₯(ballβπ·)(1 / π))) β V |
19 | 18 | elpw 4565 |
. . . . . 6
β’ (ran
(π β β β¦
(π₯(ballβπ·)(1 / π))) β π« π½ β ran (π β β β¦ (π₯(ballβπ·)(1 / π))) β π½) |
20 | 15, 19 | sylibr 233 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π₯ β π) β ran (π β β β¦ (π₯(ballβπ·)(1 / π))) β π« π½) |
21 | | omelon 9587 |
. . . . . . . . 9
β’ Ο
β On |
22 | | nnenom 13891 |
. . . . . . . . . 10
β’ β
β Ο |
23 | 22 | ensymi 8947 |
. . . . . . . . 9
β’ Ο
β β |
24 | | isnumi 9887 |
. . . . . . . . 9
β’ ((Ο
β On β§ Ο β β) β β β dom
card) |
25 | 21, 23, 24 | mp2an 691 |
. . . . . . . 8
β’ β
β dom card |
26 | | ovex 7391 |
. . . . . . . . . 10
β’ (π₯(ballβπ·)(1 / π)) β V |
27 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β β β¦ (π₯(ballβπ·)(1 / π))) = (π β β β¦ (π₯(ballβπ·)(1 / π))) |
28 | 26, 27 | fnmpti 6645 |
. . . . . . . . 9
β’ (π β β β¦ (π₯(ballβπ·)(1 / π))) Fn β |
29 | | dffn4 6763 |
. . . . . . . . 9
β’ ((π β β β¦ (π₯(ballβπ·)(1 / π))) Fn β β (π β β β¦ (π₯(ballβπ·)(1 / π))):ββontoβran (π β β β¦ (π₯(ballβπ·)(1 / π)))) |
30 | 28, 29 | mpbi 229 |
. . . . . . . 8
β’ (π β β β¦ (π₯(ballβπ·)(1 / π))):ββontoβran (π β β β¦ (π₯(ballβπ·)(1 / π))) |
31 | | fodomnum 9998 |
. . . . . . . 8
β’ (β
β dom card β ((π
β β β¦ (π₯(ballβπ·)(1 / π))):ββontoβran (π β β β¦ (π₯(ballβπ·)(1 / π))) β ran (π β β β¦ (π₯(ballβπ·)(1 / π))) βΌ β)) |
32 | 25, 30, 31 | mp2 9 |
. . . . . . 7
β’ ran
(π β β β¦
(π₯(ballβπ·)(1 / π))) βΌ β |
33 | | domentr 8956 |
. . . . . . 7
β’ ((ran
(π β β β¦
(π₯(ballβπ·)(1 / π))) βΌ β β§ β β
Ο) β ran (π
β β β¦ (π₯(ballβπ·)(1 / π))) βΌ Ο) |
34 | 32, 22, 33 | mp2an 691 |
. . . . . 6
β’ ran
(π β β β¦
(π₯(ballβπ·)(1 / π))) βΌ Ο |
35 | 34 | a1i 11 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π₯ β π) β ran (π β β β¦ (π₯(ballβπ·)(1 / π))) βΌ Ο) |
36 | | simpll 766 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β π· β (βMetβπ)) |
37 | | simprl 770 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β π§ β π½) |
38 | | simprr 772 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β π₯ β π§) |
39 | 1 | mopni2 23865 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π§ β π½ β§ π₯ β π§) β βπ β β+ (π₯(ballβπ·)π) β π§) |
40 | 36, 37, 38, 39 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β βπ β β+ (π₯(ballβπ·)π) β π§) |
41 | | simp-4l 782 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β π· β (βMetβπ)) |
42 | | simp-4r 783 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β π₯ β π) |
43 | | simprl 770 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β π¦ β β) |
44 | 43 | nnrpd 12960 |
. . . . . . . . . . . . 13
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β π¦ β β+) |
45 | 44 | rpreccld 12972 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β (1 / π¦) β
β+) |
46 | | blcntr 23782 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π₯ β π β§ (1 / π¦) β β+) β π₯ β (π₯(ballβπ·)(1 / π¦))) |
47 | 41, 42, 45, 46 | syl3anc 1372 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β π₯ β (π₯(ballβπ·)(1 / π¦))) |
48 | 45 | rpxrd 12963 |
. . . . . . . . . . . . 13
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β (1 / π¦) β
β*) |
49 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β π β β+) |
50 | 49 | rpxrd 12963 |
. . . . . . . . . . . . 13
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β π β β*) |
51 | | nnrecre 12200 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β (1 /
π¦) β
β) |
52 | 51 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β (1 / π¦) β β) |
53 | 49 | rpred 12962 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β π β β) |
54 | | simprr 772 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β (1 / π¦) < π) |
55 | 52, 53, 54 | ltled 11308 |
. . . . . . . . . . . . 13
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β (1 / π¦) β€ π) |
56 | | ssbl 23792 |
. . . . . . . . . . . . 13
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ ((1 / π¦) β β* β§ π β β*)
β§ (1 / π¦) β€ π) β (π₯(ballβπ·)(1 / π¦)) β (π₯(ballβπ·)π)) |
57 | 41, 42, 48, 50, 55, 56 | syl221anc 1382 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β (π₯(ballβπ·)(1 / π¦)) β (π₯(ballβπ·)π)) |
58 | | simplrr 777 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β (π₯(ballβπ·)π) β π§) |
59 | 57, 58 | sstrd 3955 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β (π₯(ballβπ·)(1 / π¦)) β π§) |
60 | 47, 59 | jca 513 |
. . . . . . . . . 10
β’
(((((π· β
(βMetβπ) β§
π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β§ (π¦ β β β§ (1 / π¦) < π)) β (π₯ β (π₯(ballβπ·)(1 / π¦)) β§ (π₯(ballβπ·)(1 / π¦)) β π§)) |
61 | | elrp 12922 |
. . . . . . . . . . . 12
β’ (π β β+
β (π β β
β§ 0 < π)) |
62 | | nnrecl 12416 |
. . . . . . . . . . . 12
β’ ((π β β β§ 0 <
π) β βπ¦ β β (1 / π¦) < π) |
63 | 61, 62 | sylbi 216 |
. . . . . . . . . . 11
β’ (π β β+
β βπ¦ β
β (1 / π¦) < π) |
64 | 63 | ad2antrl 727 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β βπ¦ β β (1 / π¦) < π) |
65 | 60, 64 | reximddv 3165 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ (π β β+ β§ (π₯(ballβπ·)π) β π§)) β βπ¦ β β (π₯ β (π₯(ballβπ·)(1 / π¦)) β§ (π₯(ballβπ·)(1 / π¦)) β π§)) |
66 | 40, 65 | rexlimddv 3155 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β βπ¦ β β (π₯ β (π₯(ballβπ·)(1 / π¦)) β§ (π₯(ballβπ·)(1 / π¦)) β π§)) |
67 | | ovexd 7393 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ π¦ β β) β (π₯(ballβπ·)(1 / π¦)) β V) |
68 | | vex 3448 |
. . . . . . . . . 10
β’ π€ β V |
69 | | oveq2 7366 |
. . . . . . . . . . . . 13
β’ (π = π¦ β (1 / π) = (1 / π¦)) |
70 | 69 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π = π¦ β (π₯(ballβπ·)(1 / π)) = (π₯(ballβπ·)(1 / π¦))) |
71 | 70 | cbvmptv 5219 |
. . . . . . . . . . 11
β’ (π β β β¦ (π₯(ballβπ·)(1 / π))) = (π¦ β β β¦ (π₯(ballβπ·)(1 / π¦))) |
72 | 71 | elrnmpt 5912 |
. . . . . . . . . 10
β’ (π€ β V β (π€ β ran (π β β β¦ (π₯(ballβπ·)(1 / π))) β βπ¦ β β π€ = (π₯(ballβπ·)(1 / π¦)))) |
73 | 68, 72 | mp1i 13 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β (π€ β ran (π β β β¦ (π₯(ballβπ·)(1 / π))) β βπ¦ β β π€ = (π₯(ballβπ·)(1 / π¦)))) |
74 | | eleq2 2823 |
. . . . . . . . . . 11
β’ (π€ = (π₯(ballβπ·)(1 / π¦)) β (π₯ β π€ β π₯ β (π₯(ballβπ·)(1 / π¦)))) |
75 | | sseq1 3970 |
. . . . . . . . . . 11
β’ (π€ = (π₯(ballβπ·)(1 / π¦)) β (π€ β π§ β (π₯(ballβπ·)(1 / π¦)) β π§)) |
76 | 74, 75 | anbi12d 632 |
. . . . . . . . . 10
β’ (π€ = (π₯(ballβπ·)(1 / π¦)) β ((π₯ β π€ β§ π€ β π§) β (π₯ β (π₯(ballβπ·)(1 / π¦)) β§ (π₯(ballβπ·)(1 / π¦)) β π§))) |
77 | 76 | adantl 483 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β§ π€ = (π₯(ballβπ·)(1 / π¦))) β ((π₯ β π€ β§ π€ β π§) β (π₯ β (π₯(ballβπ·)(1 / π¦)) β§ (π₯(ballβπ·)(1 / π¦)) β π§))) |
78 | 67, 73, 77 | rexxfr2d 5367 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β (βπ€ β ran (π β β β¦ (π₯(ballβπ·)(1 / π)))(π₯ β π€ β§ π€ β π§) β βπ¦ β β (π₯ β (π₯(ballβπ·)(1 / π¦)) β§ (π₯(ballβπ·)(1 / π¦)) β π§))) |
79 | 66, 78 | mpbird 257 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ (π§ β π½ β§ π₯ β π§)) β βπ€ β ran (π β β β¦ (π₯(ballβπ·)(1 / π)))(π₯ β π€ β§ π€ β π§)) |
80 | 79 | expr 458 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π₯ β π) β§ π§ β π½) β (π₯ β π§ β βπ€ β ran (π β β β¦ (π₯(ballβπ·)(1 / π)))(π₯ β π€ β§ π€ β π§))) |
81 | 80 | ralrimiva 3140 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π₯ β π) β βπ§ β π½ (π₯ β π§ β βπ€ β ran (π β β β¦ (π₯(ballβπ·)(1 / π)))(π₯ β π€ β§ π€ β π§))) |
82 | | breq1 5109 |
. . . . . . 7
β’ (π¦ = ran (π β β β¦ (π₯(ballβπ·)(1 / π))) β (π¦ βΌ Ο β ran (π β β β¦ (π₯(ballβπ·)(1 / π))) βΌ Ο)) |
83 | | rexeq 3309 |
. . . . . . . . 9
β’ (π¦ = ran (π β β β¦ (π₯(ballβπ·)(1 / π))) β (βπ€ β π¦ (π₯ β π€ β§ π€ β π§) β βπ€ β ran (π β β β¦ (π₯(ballβπ·)(1 / π)))(π₯ β π€ β§ π€ β π§))) |
84 | 83 | imbi2d 341 |
. . . . . . . 8
β’ (π¦ = ran (π β β β¦ (π₯(ballβπ·)(1 / π))) β ((π₯ β π§ β βπ€ β π¦ (π₯ β π€ β§ π€ β π§)) β (π₯ β π§ β βπ€ β ran (π β β β¦ (π₯(ballβπ·)(1 / π)))(π₯ β π€ β§ π€ β π§)))) |
85 | 84 | ralbidv 3171 |
. . . . . . 7
β’ (π¦ = ran (π β β β¦ (π₯(ballβπ·)(1 / π))) β (βπ§ β π½ (π₯ β π§ β βπ€ β π¦ (π₯ β π€ β§ π€ β π§)) β βπ§ β π½ (π₯ β π§ β βπ€ β ran (π β β β¦ (π₯(ballβπ·)(1 / π)))(π₯ β π€ β§ π€ β π§)))) |
86 | 82, 85 | anbi12d 632 |
. . . . . 6
β’ (π¦ = ran (π β β β¦ (π₯(ballβπ·)(1 / π))) β ((π¦ βΌ Ο β§ βπ§ β π½ (π₯ β π§ β βπ€ β π¦ (π₯ β π€ β§ π€ β π§))) β (ran (π β β β¦ (π₯(ballβπ·)(1 / π))) βΌ Ο β§ βπ§ β π½ (π₯ β π§ β βπ€ β ran (π β β β¦ (π₯(ballβπ·)(1 / π)))(π₯ β π€ β§ π€ β π§))))) |
87 | 86 | rspcev 3580 |
. . . . 5
β’ ((ran
(π β β β¦
(π₯(ballβπ·)(1 / π))) β π« π½ β§ (ran (π β β β¦ (π₯(ballβπ·)(1 / π))) βΌ Ο β§ βπ§ β π½ (π₯ β π§ β βπ€ β ran (π β β β¦ (π₯(ballβπ·)(1 / π)))(π₯ β π€ β§ π€ β π§)))) β βπ¦ β π« π½(π¦ βΌ Ο β§ βπ§ β π½ (π₯ β π§ β βπ€ β π¦ (π₯ β π€ β§ π€ β π§)))) |
88 | 20, 35, 81, 87 | syl12anc 836 |
. . . 4
β’ ((π· β (βMetβπ) β§ π₯ β π) β βπ¦ β π« π½(π¦ βΌ Ο β§ βπ§ β π½ (π₯ β π§ β βπ€ β π¦ (π₯ β π€ β§ π€ β π§)))) |
89 | 5, 88 | syldan 592 |
. . 3
β’ ((π· β (βMetβπ) β§ π₯ β βͺ π½) β βπ¦ β π« π½(π¦ βΌ Ο β§ βπ§ β π½ (π₯ β π§ β βπ€ β π¦ (π₯ β π€ β§ π€ β π§)))) |
90 | 89 | ralrimiva 3140 |
. 2
β’ (π· β (βMetβπ) β βπ₯ β βͺ π½βπ¦ β π« π½(π¦ βΌ Ο β§ βπ§ β π½ (π₯ β π§ β βπ€ β π¦ (π₯ β π€ β§ π€ β π§)))) |
91 | | eqid 2733 |
. . 3
β’ βͺ π½ =
βͺ π½ |
92 | 91 | is1stc2 22809 |
. 2
β’ (π½ β 1stΟ
β (π½ β Top β§
βπ₯ β βͺ π½βπ¦ β π« π½(π¦ βΌ Ο β§ βπ§ β π½ (π₯ β π§ β βπ€ β π¦ (π₯ β π€ β§ π€ β π§))))) |
93 | 2, 90, 92 | sylanbrc 584 |
1
β’ (π· β (βMetβπ) β π½ β
1stΟ) |