Step | Hyp | Ref
| Expression |
1 | | elssuni 4904 |
. . . 4
β’ (π₯ β (ordTopβ β€ )
β π₯ β βͺ (ordTopβ β€ )) |
2 | | letopuni 22596 |
. . . 4
β’
β* = βͺ (ordTopβ β€
) |
3 | 1, 2 | sseqtrrdi 3999 |
. . 3
β’ (π₯ β (ordTopβ β€ )
β π₯ β
β*) |
4 | | eqid 2732 |
. . . . . . . 8
β’ ((abs
β β ) βΎ (β Γ β)) = ((abs β β )
βΎ (β Γ β)) |
5 | 4 | rexmet 24192 |
. . . . . . 7
β’ ((abs
β β ) βΎ (β Γ β)) β
(βMetββ) |
6 | | letop 22595 |
. . . . . . . . 9
β’
(ordTopβ β€ ) β Top |
7 | | reex 11152 |
. . . . . . . . 9
β’ β
β V |
8 | | elrestr 17325 |
. . . . . . . . 9
β’
(((ordTopβ β€ ) β Top β§ β β V β§ π₯ β (ordTopβ β€ ))
β (π₯ β© β)
β ((ordTopβ β€ ) βΎt β)) |
9 | 6, 7, 8 | mp3an12 1452 |
. . . . . . . 8
β’ (π₯ β (ordTopβ β€ )
β (π₯ β© β)
β ((ordTopβ β€ ) βΎt β)) |
10 | 9 | ad2antrr 725 |
. . . . . . 7
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β (π₯ β© β) β ((ordTopβ β€ )
βΎt β)) |
11 | | elin 3930 |
. . . . . . . . 9
β’ (π¦ β (π₯ β© β) β (π¦ β π₯ β§ π¦ β β)) |
12 | 11 | biimpri 227 |
. . . . . . . 8
β’ ((π¦ β π₯ β§ π¦ β β) β π¦ β (π₯ β© β)) |
13 | 12 | adantll 713 |
. . . . . . 7
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β π¦ β (π₯ β© β)) |
14 | | eqid 2732 |
. . . . . . . . . 10
β’
((ordTopβ β€ ) βΎt β) = ((ordTopβ
β€ ) βΎt β) |
15 | 14 | xrtgioo 24207 |
. . . . . . . . 9
β’
(topGenβran (,)) = ((ordTopβ β€ ) βΎt
β) |
16 | | eqid 2732 |
. . . . . . . . . 10
β’
(MetOpenβ((abs β β ) βΎ (β Γ
β))) = (MetOpenβ((abs β β ) βΎ (β Γ
β))) |
17 | 4, 16 | tgioo 24197 |
. . . . . . . . 9
β’
(topGenβran (,)) = (MetOpenβ((abs β β ) βΎ
(β Γ β))) |
18 | 15, 17 | eqtr3i 2762 |
. . . . . . . 8
β’
((ordTopβ β€ ) βΎt β) =
(MetOpenβ((abs β β ) βΎ (β Γ
β))) |
19 | 18 | mopni2 23887 |
. . . . . . 7
β’ ((((abs
β β ) βΎ (β Γ β)) β
(βMetββ) β§ (π₯ β© β) β ((ordTopβ β€ )
βΎt β) β§ π¦ β (π₯ β© β)) β βπ β β+
(π¦(ballβ((abs β
β ) βΎ (β Γ β)))π) β (π₯ β© β)) |
20 | 5, 10, 13, 19 | mp3an2i 1467 |
. . . . . 6
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β βπ β β+
(π¦(ballβ((abs β
β ) βΎ (β Γ β)))π) β (π₯ β© β)) |
21 | | xrsxmet.1 |
. . . . . . . . . . . 12
β’ π· =
(distββ*π ) |
22 | 21 | xrsxmet 24210 |
. . . . . . . . . . 11
β’ π· β
(βMetββ*) |
23 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β§ π β β+) β π¦ β
β) |
24 | | ressxr 11209 |
. . . . . . . . . . . . 13
β’ β
β β* |
25 | | sseqin2 4181 |
. . . . . . . . . . . . 13
β’ (β
β β* β (β* β© β) =
β) |
26 | 24, 25 | mpbi 229 |
. . . . . . . . . . . 12
β’
(β* β© β) = β |
27 | 23, 26 | eleqtrrdi 2844 |
. . . . . . . . . . 11
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β§ π β β+) β π¦ β (β*
β© β)) |
28 | | rpxr 12934 |
. . . . . . . . . . . 12
β’ (π β β+
β π β
β*) |
29 | 28 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β§ π β β+) β π β
β*) |
30 | 21 | xrsdsre 24211 |
. . . . . . . . . . . . 13
β’ (π· βΎ (β Γ
β)) = ((abs β β ) βΎ (β Γ
β)) |
31 | 30 | eqcomi 2741 |
. . . . . . . . . . . 12
β’ ((abs
β β ) βΎ (β Γ β)) = (π· βΎ (β Γ
β)) |
32 | 31 | blres 23822 |
. . . . . . . . . . 11
β’ ((π· β
(βMetββ*) β§ π¦ β (β* β© β)
β§ π β
β*) β (π¦(ballβ((abs β β ) βΎ
(β Γ β)))π) = ((π¦(ballβπ·)π) β© β)) |
33 | 22, 27, 29, 32 | mp3an2i 1467 |
. . . . . . . . . 10
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β§ π β β+) β (π¦(ballβ((abs β
β ) βΎ (β Γ β)))π) = ((π¦(ballβπ·)π) β© β)) |
34 | 21 | xrsblre 24212 |
. . . . . . . . . . . . 13
β’ ((π¦ β β β§ π β β*)
β (π¦(ballβπ·)π) β β) |
35 | 28, 34 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((π¦ β β β§ π β β+)
β (π¦(ballβπ·)π) β β) |
36 | 35 | adantll 713 |
. . . . . . . . . . 11
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β§ π β β+) β (π¦(ballβπ·)π) β β) |
37 | | df-ss 3931 |
. . . . . . . . . . 11
β’ ((π¦(ballβπ·)π) β β β ((π¦(ballβπ·)π) β© β) = (π¦(ballβπ·)π)) |
38 | 36, 37 | sylib 217 |
. . . . . . . . . 10
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β§ π β β+) β ((π¦(ballβπ·)π) β© β) = (π¦(ballβπ·)π)) |
39 | 33, 38 | eqtrd 2772 |
. . . . . . . . 9
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β§ π β β+) β (π¦(ballβ((abs β
β ) βΎ (β Γ β)))π) = (π¦(ballβπ·)π)) |
40 | 39 | sseq1d 3979 |
. . . . . . . 8
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β§ π β β+) β ((π¦(ballβ((abs β
β ) βΎ (β Γ β)))π) β (π₯ β© β) β (π¦(ballβπ·)π) β (π₯ β© β))) |
41 | | inss1 4194 |
. . . . . . . . 9
β’ (π₯ β© β) β π₯ |
42 | | sstr 3956 |
. . . . . . . . 9
β’ (((π¦(ballβπ·)π) β (π₯ β© β) β§ (π₯ β© β) β π₯) β (π¦(ballβπ·)π) β π₯) |
43 | 41, 42 | mpan2 690 |
. . . . . . . 8
β’ ((π¦(ballβπ·)π) β (π₯ β© β) β (π¦(ballβπ·)π) β π₯) |
44 | 40, 43 | syl6bi 253 |
. . . . . . 7
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β§ π β β+) β ((π¦(ballβ((abs β
β ) βΎ (β Γ β)))π) β (π₯ β© β) β (π¦(ballβπ·)π) β π₯)) |
45 | 44 | reximdva 3162 |
. . . . . 6
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β (βπ β β+
(π¦(ballβ((abs β
β ) βΎ (β Γ β)))π) β (π₯ β© β) β βπ β β+
(π¦(ballβπ·)π) β π₯)) |
46 | 20, 45 | mpd 15 |
. . . . 5
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ π¦ β β) β βπ β β+
(π¦(ballβπ·)π) β π₯) |
47 | | 1rp 12929 |
. . . . . 6
β’ 1 β
β+ |
48 | 3 | sselda 3948 |
. . . . . . . . . 10
β’ ((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β π¦ β β*) |
49 | 48 | adantr 482 |
. . . . . . . . 9
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β) β π¦ β β*) |
50 | | rpxr 12934 |
. . . . . . . . . 10
β’ (1 β
β+ β 1 β β*) |
51 | 47, 50 | mp1i 13 |
. . . . . . . . 9
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β) β 1 β
β*) |
52 | | elbl 23779 |
. . . . . . . . 9
β’ ((π· β
(βMetββ*) β§ π¦ β β* β§ 1 β
β*) β (π§ β (π¦(ballβπ·)1) β (π§ β β* β§ (π¦π·π§) < 1))) |
53 | 22, 49, 51, 52 | mp3an2i 1467 |
. . . . . . . 8
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β) β (π§ β (π¦(ballβπ·)1) β (π§ β β* β§ (π¦π·π§) < 1))) |
54 | | simp2 1138 |
. . . . . . . . . 10
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β Β¬ π¦ β β) |
55 | 48 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β π¦ β β*) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β π¦ β β*) |
57 | | simpl3l 1229 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β π§ β β*) |
58 | | xmetcl 23722 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β
(βMetββ*) β§ π¦ β β* β§ π§ β β*)
β (π¦π·π§) β
β*) |
59 | 22, 56, 57, 58 | mp3an2i 1467 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β (π¦π·π§) β
β*) |
60 | | 1red 11166 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β 1 β β) |
61 | | xmetge0 23735 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β
(βMetββ*) β§ π¦ β β* β§ π§ β β*)
β 0 β€ (π¦π·π§)) |
62 | 22, 56, 57, 61 | mp3an2i 1467 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β 0 β€ (π¦π·π§)) |
63 | | simpl3r 1230 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β (π¦π·π§) < 1) |
64 | | 1xr 11224 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β* |
65 | | xrltle 13079 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦π·π§) β β* β§ 1 β
β*) β ((π¦π·π§) < 1 β (π¦π·π§) β€ 1)) |
66 | 59, 64, 65 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β ((π¦π·π§) < 1 β (π¦π·π§) β€ 1)) |
67 | 63, 66 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β (π¦π·π§) β€ 1) |
68 | | xrrege0 13104 |
. . . . . . . . . . . . . . . 16
β’ ((((π¦π·π§) β β* β§ 1 β
β) β§ (0 β€ (π¦π·π§) β§ (π¦π·π§) β€ 1)) β (π¦π·π§) β β) |
69 | 59, 60, 62, 67, 68 | syl22anc 838 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β (π¦π·π§) β β) |
70 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β π¦ β π§) |
71 | 21 | xrsdsreclb 20882 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β β*
β§ π§ β
β* β§ π¦
β π§) β ((π¦π·π§) β β β (π¦ β β β§ π§ β β))) |
72 | 56, 57, 70, 71 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β ((π¦π·π§) β β β (π¦ β β β§ π§ β β))) |
73 | 69, 72 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β (π¦ β β β§ π§ β β)) |
74 | 73 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β§ π¦ β π§) β π¦ β β) |
75 | 74 | ex 414 |
. . . . . . . . . . . 12
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β (π¦ β π§ β π¦ β β)) |
76 | 75 | necon1bd 2958 |
. . . . . . . . . . 11
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β (Β¬ π¦ β β β π¦ = π§)) |
77 | | simp1r 1199 |
. . . . . . . . . . . 12
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β π¦ β π₯) |
78 | | elequ1 2114 |
. . . . . . . . . . . 12
β’ (π¦ = π§ β (π¦ β π₯ β π§ β π₯)) |
79 | 77, 78 | syl5ibcom 244 |
. . . . . . . . . . 11
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β (π¦ = π§ β π§ β π₯)) |
80 | 76, 79 | syld 47 |
. . . . . . . . . 10
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β (Β¬ π¦ β β β π§ β π₯)) |
81 | 54, 80 | mpd 15 |
. . . . . . . . 9
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β β§ (π§ β β* β§ (π¦π·π§) < 1)) β π§ β π₯) |
82 | 81 | 3expia 1122 |
. . . . . . . 8
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β) β ((π§ β β* β§ (π¦π·π§) < 1) β π§ β π₯)) |
83 | 53, 82 | sylbid 239 |
. . . . . . 7
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β) β (π§ β (π¦(ballβπ·)1) β π§ β π₯)) |
84 | 83 | ssrdv 3954 |
. . . . . 6
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β) β (π¦(ballβπ·)1) β π₯) |
85 | | oveq2 7371 |
. . . . . . . 8
β’ (π = 1 β (π¦(ballβπ·)π) = (π¦(ballβπ·)1)) |
86 | 85 | sseq1d 3979 |
. . . . . . 7
β’ (π = 1 β ((π¦(ballβπ·)π) β π₯ β (π¦(ballβπ·)1) β π₯)) |
87 | 86 | rspcev 3583 |
. . . . . 6
β’ ((1
β β+ β§ (π¦(ballβπ·)1) β π₯) β βπ β β+ (π¦(ballβπ·)π) β π₯) |
88 | 47, 84, 87 | sylancr 588 |
. . . . 5
β’ (((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β§ Β¬ π¦ β β) β βπ β β+
(π¦(ballβπ·)π) β π₯) |
89 | 46, 88 | pm2.61dan 812 |
. . . 4
β’ ((π₯ β (ordTopβ β€ )
β§ π¦ β π₯) β βπ β β+
(π¦(ballβπ·)π) β π₯) |
90 | 89 | ralrimiva 3140 |
. . 3
β’ (π₯ β (ordTopβ β€ )
β βπ¦ β
π₯ βπ β β+ (π¦(ballβπ·)π) β π₯) |
91 | | xrsmopn.1 |
. . . . 5
β’ π½ = (MetOpenβπ·) |
92 | 91 | elmopn2 23836 |
. . . 4
β’ (π· β
(βMetββ*) β (π₯ β π½ β (π₯ β β* β§
βπ¦ β π₯ βπ β β+ (π¦(ballβπ·)π) β π₯))) |
93 | 22, 92 | ax-mp 5 |
. . 3
β’ (π₯ β π½ β (π₯ β β* β§
βπ¦ β π₯ βπ β β+ (π¦(ballβπ·)π) β π₯)) |
94 | 3, 90, 93 | sylanbrc 584 |
. 2
β’ (π₯ β (ordTopβ β€ )
β π₯ β π½) |
95 | 94 | ssriv 3952 |
1
β’
(ordTopβ β€ ) β π½ |