Step | Hyp | Ref
| Expression |
1 | | restsspw 17321 |
. 2
β’ (π½ βΎt β€)
β π« β€ |
2 | | elpwi 4571 |
. . . . . . . . 9
β’ (π₯ β π« β€ β
π₯ β
β€) |
3 | 2 | sselda 3948 |
. . . . . . . 8
β’ ((π₯ β π« β€ β§
π¦ β π₯) β π¦ β β€) |
4 | 3 | zcnd 12616 |
. . . . . . 7
β’ ((π₯ β π« β€ β§
π¦ β π₯) β π¦ β β) |
5 | | cnxmet 24159 |
. . . . . . . 8
β’ (abs
β β ) β (βMetββ) |
6 | | 1xr 11222 |
. . . . . . . 8
β’ 1 β
β* |
7 | | recld2.1 |
. . . . . . . . . 10
β’ π½ =
(TopOpenββfld) |
8 | 7 | cnfldtopn 24168 |
. . . . . . . . 9
β’ π½ = (MetOpenβ(abs β
β )) |
9 | 8 | blopn 23879 |
. . . . . . . 8
β’ (((abs
β β ) β (βMetββ) β§ π¦ β β β§ 1 β
β*) β (π¦(ballβ(abs β β ))1) β
π½) |
10 | 5, 6, 9 | mp3an13 1453 |
. . . . . . 7
β’ (π¦ β β β (π¦(ballβ(abs β β
))1) β π½) |
11 | 7 | cnfldtop 24170 |
. . . . . . . 8
β’ π½ β Top |
12 | | zex 12516 |
. . . . . . . 8
β’ β€
β V |
13 | | elrestr 17318 |
. . . . . . . 8
β’ ((π½ β Top β§ β€ β
V β§ (π¦(ballβ(abs
β β ))1) β π½) β ((π¦(ballβ(abs β β ))1) β©
β€) β (π½
βΎt β€)) |
14 | 11, 12, 13 | mp3an12 1452 |
. . . . . . 7
β’ ((π¦(ballβ(abs β β
))1) β π½ β
((π¦(ballβ(abs β
β ))1) β© β€) β (π½ βΎt
β€)) |
15 | 4, 10, 14 | 3syl 18 |
. . . . . 6
β’ ((π₯ β π« β€ β§
π¦ β π₯) β ((π¦(ballβ(abs β β ))1) β©
β€) β (π½
βΎt β€)) |
16 | | 1rp 12927 |
. . . . . . . . 9
β’ 1 β
β+ |
17 | | blcntr 23789 |
. . . . . . . . 9
β’ (((abs
β β ) β (βMetββ) β§ π¦ β β β§ 1 β
β+) β π¦ β (π¦(ballβ(abs β β
))1)) |
18 | 5, 16, 17 | mp3an13 1453 |
. . . . . . . 8
β’ (π¦ β β β π¦ β (π¦(ballβ(abs β β
))1)) |
19 | 4, 18 | syl 17 |
. . . . . . 7
β’ ((π₯ β π« β€ β§
π¦ β π₯) β π¦ β (π¦(ballβ(abs β β
))1)) |
20 | 19, 3 | elind 4158 |
. . . . . 6
β’ ((π₯ β π« β€ β§
π¦ β π₯) β π¦ β ((π¦(ballβ(abs β β ))1) β©
β€)) |
21 | 4 | adantr 482 |
. . . . . . . . . 10
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β π¦ β
β) |
22 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β π§ β
((π¦(ballβ(abs β
β ))1) β© β€)) |
23 | 22 | elin2d 4163 |
. . . . . . . . . . 11
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β π§ β
β€) |
24 | 23 | zcnd 12616 |
. . . . . . . . . 10
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β π§ β
β) |
25 | 3 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β π¦ β
β€) |
26 | 25, 23 | zsubcld 12620 |
. . . . . . . . . . . 12
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β (π¦ β
π§) β
β€) |
27 | 26 | zcnd 12616 |
. . . . . . . . . . 11
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β (π¦ β
π§) β
β) |
28 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (abs
β β ) = (abs β β ) |
29 | 28 | cnmetdval 24157 |
. . . . . . . . . . . . . 14
β’ ((π¦ β β β§ π§ β β) β (π¦(abs β β )π§) = (absβ(π¦ β π§))) |
30 | 21, 24, 29 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β (π¦(abs
β β )π§) =
(absβ(π¦ β π§))) |
31 | 22 | elin1d 4162 |
. . . . . . . . . . . . . 14
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β π§ β
(π¦(ballβ(abs β
β ))1)) |
32 | | elbl2 23766 |
. . . . . . . . . . . . . . . 16
β’ ((((abs
β β ) β (βMetββ) β§ 1 β
β*) β§ (π¦ β β β§ π§ β β)) β (π§ β (π¦(ballβ(abs β β ))1) β
(π¦(abs β β
)π§) <
1)) |
33 | 5, 6, 32 | mpanl12 701 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β β§ π§ β β) β (π§ β (π¦(ballβ(abs β β ))1) β
(π¦(abs β β
)π§) <
1)) |
34 | 21, 24, 33 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β (π§ β
(π¦(ballβ(abs β
β ))1) β (π¦(abs
β β )π§) <
1)) |
35 | 31, 34 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β (π¦(abs
β β )π§) <
1) |
36 | 30, 35 | eqbrtrrd 5133 |
. . . . . . . . . . . 12
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β (absβ(π¦ β π§)) < 1) |
37 | | nn0abscl 15206 |
. . . . . . . . . . . . 13
β’ ((π¦ β π§) β β€ β (absβ(π¦ β π§)) β
β0) |
38 | | nn0lt10b 12573 |
. . . . . . . . . . . . 13
β’
((absβ(π¦
β π§)) β
β0 β ((absβ(π¦ β π§)) < 1 β (absβ(π¦ β π§)) = 0)) |
39 | 26, 37, 38 | 3syl 18 |
. . . . . . . . . . . 12
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β ((absβ(π¦ β π§)) < 1 β (absβ(π¦ β π§)) = 0)) |
40 | 36, 39 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β (absβ(π¦ β π§)) = 0) |
41 | 27, 40 | abs00d 15340 |
. . . . . . . . . 10
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β (π¦ β
π§) = 0) |
42 | 21, 24, 41 | subeq0d 11528 |
. . . . . . . . 9
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β π¦ = π§) |
43 | | simplr 768 |
. . . . . . . . 9
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β π¦ β
π₯) |
44 | 42, 43 | eqeltrrd 2835 |
. . . . . . . 8
β’ (((π₯ β π« β€ β§
π¦ β π₯) β§ π§ β ((π¦(ballβ(abs β β ))1) β©
β€)) β π§ β
π₯) |
45 | 44 | ex 414 |
. . . . . . 7
β’ ((π₯ β π« β€ β§
π¦ β π₯) β (π§ β ((π¦(ballβ(abs β β ))1) β©
β€) β π§ β
π₯)) |
46 | 45 | ssrdv 3954 |
. . . . . 6
β’ ((π₯ β π« β€ β§
π¦ β π₯) β ((π¦(ballβ(abs β β ))1) β©
β€) β π₯) |
47 | | eleq2 2823 |
. . . . . . . 8
β’ (π§ = ((π¦(ballβ(abs β β ))1) β©
β€) β (π¦ β
π§ β π¦ β ((π¦(ballβ(abs β β ))1) β©
β€))) |
48 | | sseq1 3973 |
. . . . . . . 8
β’ (π§ = ((π¦(ballβ(abs β β ))1) β©
β€) β (π§ β
π₯ β ((π¦(ballβ(abs β β
))1) β© β€) β π₯)) |
49 | 47, 48 | anbi12d 632 |
. . . . . . 7
β’ (π§ = ((π¦(ballβ(abs β β ))1) β©
β€) β ((π¦ β
π§ β§ π§ β π₯) β (π¦ β ((π¦(ballβ(abs β β ))1) β©
β€) β§ ((π¦(ballβ(abs β β ))1) β©
β€) β π₯))) |
50 | 49 | rspcev 3583 |
. . . . . 6
β’ ((((π¦(ballβ(abs β β
))1) β© β€) β (π½ βΎt β€) β§ (π¦ β ((π¦(ballβ(abs β β ))1) β©
β€) β§ ((π¦(ballβ(abs β β ))1) β©
β€) β π₯)) β
βπ§ β (π½ βΎt
β€)(π¦ β π§ β§ π§ β π₯)) |
51 | 15, 20, 46, 50 | syl12anc 836 |
. . . . 5
β’ ((π₯ β π« β€ β§
π¦ β π₯) β βπ§ β (π½ βΎt β€)(π¦ β π§ β§ π§ β π₯)) |
52 | 51 | ralrimiva 3140 |
. . . 4
β’ (π₯ β π« β€ β
βπ¦ β π₯ βπ§ β (π½ βΎt β€)(π¦ β π§ β§ π§ β π₯)) |
53 | | resttop 22534 |
. . . . . 6
β’ ((π½ β Top β§ β€ β
V) β (π½
βΎt β€) β Top) |
54 | 11, 12, 53 | mp2an 691 |
. . . . 5
β’ (π½ βΎt β€)
β Top |
55 | | eltop2 22348 |
. . . . 5
β’ ((π½ βΎt β€)
β Top β (π₯ β
(π½ βΎt
β€) β βπ¦
β π₯ βπ§ β (π½ βΎt β€)(π¦ β π§ β§ π§ β π₯))) |
56 | 54, 55 | ax-mp 5 |
. . . 4
β’ (π₯ β (π½ βΎt β€) β
βπ¦ β π₯ βπ§ β (π½ βΎt β€)(π¦ β π§ β§ π§ β π₯)) |
57 | 52, 56 | sylibr 233 |
. . 3
β’ (π₯ β π« β€ β
π₯ β (π½ βΎt
β€)) |
58 | 57 | ssriv 3952 |
. 2
β’ π«
β€ β (π½
βΎt β€) |
59 | 1, 58 | eqssi 3964 |
1
β’ (π½ βΎt β€) =
π« β€ |