Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
β’
(TopOpenββfld) =
(TopOpenββfld) |
2 | 1 | cnfldtopn 24148 |
. . . 4
β’
(TopOpenββfld) = (MetOpenβ(abs β
β )) |
3 | | cncmet.1 |
. . . . 5
β’ π· = (abs β β
) |
4 | 3 | fveq2i 6846 |
. . . 4
β’
(MetOpenβπ·) =
(MetOpenβ(abs β β )) |
5 | 2, 4 | eqtr4i 2768 |
. . 3
β’
(TopOpenββfld) = (MetOpenβπ·) |
6 | | cnmet 24138 |
. . . . 5
β’ (abs
β β ) β (Metββ) |
7 | 3, 6 | eqeltri 2834 |
. . . 4
β’ π· β
(Metββ) |
8 | 7 | a1i 11 |
. . 3
β’ (β€
β π· β
(Metββ)) |
9 | | 1rp 12920 |
. . . 4
β’ 1 β
β+ |
10 | 9 | a1i 11 |
. . 3
β’ (β€
β 1 β β+) |
11 | 1 | cnfldtop 24150 |
. . . . . 6
β’
(TopOpenββfld) β Top |
12 | | metxmet 23690 |
. . . . . . . 8
β’ (π· β (Metββ)
β π· β
(βMetββ)) |
13 | 7, 12 | ax-mp 5 |
. . . . . . 7
β’ π· β
(βMetββ) |
14 | | 1xr 11215 |
. . . . . . 7
β’ 1 β
β* |
15 | | blssm 23774 |
. . . . . . 7
β’ ((π· β
(βMetββ) β§ π₯ β β β§ 1 β
β*) β (π₯(ballβπ·)1) β β) |
16 | 13, 14, 15 | mp3an13 1453 |
. . . . . 6
β’ (π₯ β β β (π₯(ballβπ·)1) β β) |
17 | | unicntop 24152 |
. . . . . . 7
β’ β =
βͺ
(TopOpenββfld) |
18 | 17 | clscld 22401 |
. . . . . 6
β’
(((TopOpenββfld) β Top β§ (π₯(ballβπ·)1) β β) β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1)) β
(Clsdβ(TopOpenββfld))) |
19 | 11, 16, 18 | sylancr 588 |
. . . . 5
β’ (π₯ β β β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1)) β
(Clsdβ(TopOpenββfld))) |
20 | | abscl 15164 |
. . . . . . 7
β’ (π₯ β β β
(absβπ₯) β
β) |
21 | | peano2re 11329 |
. . . . . . 7
β’
((absβπ₯)
β β β ((absβπ₯) + 1) β β) |
22 | 20, 21 | syl 17 |
. . . . . 6
β’ (π₯ β β β
((absβπ₯) + 1) β
β) |
23 | | df-rab 3409 |
. . . . . . . . . . 11
β’ {π¦ β β β£ (π₯π·π¦) β€ 1} = {π¦ β£ (π¦ β β β§ (π₯π·π¦) β€ 1)} |
24 | 23 | eqcomi 2746 |
. . . . . . . . . 10
β’ {π¦ β£ (π¦ β β β§ (π₯π·π¦) β€ 1)} = {π¦ β β β£ (π₯π·π¦) β€ 1} |
25 | 5, 24 | blcls 23865 |
. . . . . . . . 9
β’ ((π· β
(βMetββ) β§ π₯ β β β§ 1 β
β*) β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1)) β {π¦ β£ (π¦ β β β§ (π₯π·π¦) β€ 1)}) |
26 | 13, 14, 25 | mp3an13 1453 |
. . . . . . . 8
β’ (π₯ β β β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1)) β {π¦ β£ (π¦ β β β§ (π₯π·π¦) β€ 1)}) |
27 | | abscl 15164 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β
(absβπ¦) β
β) |
28 | 27 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β (absβπ¦) β
β) |
29 | 20 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β (absβπ₯) β
β) |
30 | 28, 29 | resubcld 11584 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β ((absβπ¦) β (absβπ₯)) β
β) |
31 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π¦ β β β§ (π₯π·π¦) β€ 1) β π¦ β β) |
32 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β π₯ β
β) |
33 | | subcl 11401 |
. . . . . . . . . . . . . 14
β’ ((π¦ β β β§ π₯ β β) β (π¦ β π₯) β β) |
34 | 31, 32, 33 | syl2anr 598 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β (π¦ β π₯) β β) |
35 | 34 | abscld 15322 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β (absβ(π¦ β π₯)) β β) |
36 | | 1red 11157 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β 1 β
β) |
37 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β π¦ β β) |
38 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β π₯ β β) |
39 | 37, 38 | abs2difd 15343 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β ((absβπ¦) β (absβπ₯)) β€ (absβ(π¦ β π₯))) |
40 | 3 | cnmetdval 24137 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π¦ β β) β (π₯π·π¦) = (absβ(π₯ β π¦))) |
41 | | abssub 15212 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π¦ β β) β
(absβ(π₯ β π¦)) = (absβ(π¦ β π₯))) |
42 | 40, 41 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π¦ β β) β (π₯π·π¦) = (absβ(π¦ β π₯))) |
43 | 42 | adantrr 716 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β (π₯π·π¦) = (absβ(π¦ β π₯))) |
44 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β (π₯π·π¦) β€ 1) |
45 | 43, 44 | eqbrtrrd 5130 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β (absβ(π¦ β π₯)) β€ 1) |
46 | 30, 35, 36, 39, 45 | letrd 11313 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β ((absβπ¦) β (absβπ₯)) β€ 1) |
47 | 28, 29, 36 | lesubadd2d 11755 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β (((absβπ¦) β (absβπ₯)) β€ 1 β
(absβπ¦) β€
((absβπ₯) +
1))) |
48 | 46, 47 | mpbid 231 |
. . . . . . . . . 10
β’ ((π₯ β β β§ (π¦ β β β§ (π₯π·π¦) β€ 1)) β (absβπ¦) β€ ((absβπ₯) + 1)) |
49 | 48 | ex 414 |
. . . . . . . . 9
β’ (π₯ β β β ((π¦ β β β§ (π₯π·π¦) β€ 1) β (absβπ¦) β€ ((absβπ₯) + 1))) |
50 | 49 | ss2abdv 4021 |
. . . . . . . 8
β’ (π₯ β β β {π¦ β£ (π¦ β β β§ (π₯π·π¦) β€ 1)} β {π¦ β£ (absβπ¦) β€ ((absβπ₯) + 1)}) |
51 | 26, 50 | sstrd 3955 |
. . . . . . 7
β’ (π₯ β β β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1)) β {π¦ β£ (absβπ¦) β€ ((absβπ₯) + 1)}) |
52 | | ssabral 4020 |
. . . . . . 7
β’
(((clsβ(TopOpenββfld))β(π₯(ballβπ·)1)) β {π¦ β£ (absβπ¦) β€ ((absβπ₯) + 1)} β βπ¦ β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))(absβπ¦) β€ ((absβπ₯) + 1)) |
53 | 51, 52 | sylib 217 |
. . . . . 6
β’ (π₯ β β β
βπ¦ β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))(absβπ¦) β€ ((absβπ₯) + 1)) |
54 | | brralrspcev 5166 |
. . . . . 6
β’
((((absβπ₯) +
1) β β β§ βπ¦ β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))(absβπ¦) β€ ((absβπ₯) + 1)) β βπ β β βπ¦ β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))(absβπ¦) β€ π) |
55 | 22, 53, 54 | syl2anc 585 |
. . . . 5
β’ (π₯ β β β
βπ β β
βπ¦ β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))(absβπ¦) β€ π) |
56 | 17 | clsss3 22413 |
. . . . . . 7
β’
(((TopOpenββfld) β Top β§ (π₯(ballβπ·)1) β β) β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1)) β β) |
57 | 11, 16, 56 | sylancr 588 |
. . . . . 6
β’ (π₯ β β β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1)) β β) |
58 | | eqid 2737 |
. . . . . . 7
β’
((TopOpenββfld) βΎt
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))) =
((TopOpenββfld) βΎt
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))) |
59 | 1, 58 | cnheibor 24321 |
. . . . . 6
β’
(((clsβ(TopOpenββfld))β(π₯(ballβπ·)1)) β β β
(((TopOpenββfld) βΎt
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))) β Comp β
(((clsβ(TopOpenββfld))β(π₯(ballβπ·)1)) β
(Clsdβ(TopOpenββfld)) β§ βπ β β βπ¦ β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))(absβπ¦) β€ π))) |
60 | 57, 59 | syl 17 |
. . . . 5
β’ (π₯ β β β
(((TopOpenββfld) βΎt
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))) β Comp β
(((clsβ(TopOpenββfld))β(π₯(ballβπ·)1)) β
(Clsdβ(TopOpenββfld)) β§ βπ β β βπ¦ β
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))(absβπ¦) β€ π))) |
61 | 19, 55, 60 | mpbir2and 712 |
. . . 4
β’ (π₯ β β β
((TopOpenββfld) βΎt
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))) β Comp) |
62 | 61 | adantl 483 |
. . 3
β’
((β€ β§ π₯
β β) β ((TopOpenββfld)
βΎt
((clsβ(TopOpenββfld))β(π₯(ballβπ·)1))) β Comp) |
63 | 5, 8, 10, 62 | relcmpcmet 24685 |
. 2
β’ (β€
β π· β
(CMetββ)) |
64 | 63 | mptru 1549 |
1
β’ π· β
(CMetββ) |