Step | Hyp | Ref
| Expression |
1 | | ismtyhmeolem.5 |
. . . . 5
β’ (π β πΉ β (π Ismty π)) |
2 | | ismtyhmeolem.3 |
. . . . . 6
β’ (π β π β (βMetβπ)) |
3 | | ismtyhmeolem.4 |
. . . . . 6
β’ (π β π β (βMetβπ)) |
4 | | isismty 36973 |
. . . . . 6
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (πΉ β (π Ismty π) β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))))) |
5 | 2, 3, 4 | syl2anc 583 |
. . . . 5
β’ (π β (πΉ β (π Ismty π) β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))))) |
6 | 1, 5 | mpbid 231 |
. . . 4
β’ (π β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) |
7 | 6 | simpld 494 |
. . 3
β’ (π β πΉ:πβ1-1-ontoβπ) |
8 | | f1of 6833 |
. . 3
β’ (πΉ:πβ1-1-ontoβπ β πΉ:πβΆπ) |
9 | 7, 8 | syl 17 |
. 2
β’ (π β πΉ:πβΆπ) |
10 | 3 | adantr 480 |
. . . . . . 7
β’ ((π β§ (π€ β π β§ π β β*)) β π β (βMetβπ)) |
11 | 2 | adantr 480 |
. . . . . . 7
β’ ((π β§ (π€ β π β§ π β β*)) β π β (βMetβπ)) |
12 | | ismtycnv 36974 |
. . . . . . . . . 10
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (πΉ β (π Ismty π) β β‘πΉ β (π Ismty π))) |
13 | 2, 3, 12 | syl2anc 583 |
. . . . . . . . 9
β’ (π β (πΉ β (π Ismty π) β β‘πΉ β (π Ismty π))) |
14 | 1, 13 | mpd 15 |
. . . . . . . 8
β’ (π β β‘πΉ β (π Ismty π)) |
15 | 14 | adantr 480 |
. . . . . . 7
β’ ((π β§ (π€ β π β§ π β β*)) β β‘πΉ β (π Ismty π)) |
16 | | simprl 768 |
. . . . . . 7
β’ ((π β§ (π€ β π β§ π β β*)) β π€ β π) |
17 | | simprr 770 |
. . . . . . 7
β’ ((π β§ (π€ β π β§ π β β*)) β π β
β*) |
18 | | ismtyima 36975 |
. . . . . . 7
β’ (((π β (βMetβπ) β§ π β (βMetβπ) β§ β‘πΉ β (π Ismty π)) β§ (π€ β π β§ π β β*)) β (β‘πΉ β (π€(ballβπ)π)) = ((β‘πΉβπ€)(ballβπ)π)) |
19 | 10, 11, 15, 16, 17, 18 | syl32anc 1377 |
. . . . . 6
β’ ((π β§ (π€ β π β§ π β β*)) β (β‘πΉ β (π€(ballβπ)π)) = ((β‘πΉβπ€)(ballβπ)π)) |
20 | | f1ocnv 6845 |
. . . . . . . . 9
β’ (πΉ:πβ1-1-ontoβπ β β‘πΉ:πβ1-1-ontoβπ) |
21 | | f1of 6833 |
. . . . . . . . 9
β’ (β‘πΉ:πβ1-1-ontoβπ β β‘πΉ:πβΆπ) |
22 | 7, 20, 21 | 3syl 18 |
. . . . . . . 8
β’ (π β β‘πΉ:πβΆπ) |
23 | | simpl 482 |
. . . . . . . 8
β’ ((π€ β π β§ π β β*) β π€ β π) |
24 | | ffvelcdm 7083 |
. . . . . . . 8
β’ ((β‘πΉ:πβΆπ β§ π€ β π) β (β‘πΉβπ€) β π) |
25 | 22, 23, 24 | syl2an 595 |
. . . . . . 7
β’ ((π β§ (π€ β π β§ π β β*)) β (β‘πΉβπ€) β π) |
26 | | ismtyhmeo.1 |
. . . . . . . 8
β’ π½ = (MetOpenβπ) |
27 | 26 | blopn 24230 |
. . . . . . 7
β’ ((π β (βMetβπ) β§ (β‘πΉβπ€) β π β§ π β β*) β ((β‘πΉβπ€)(ballβπ)π) β π½) |
28 | 11, 25, 17, 27 | syl3anc 1370 |
. . . . . 6
β’ ((π β§ (π€ β π β§ π β β*)) β ((β‘πΉβπ€)(ballβπ)π) β π½) |
29 | 19, 28 | eqeltrd 2832 |
. . . . 5
β’ ((π β§ (π€ β π β§ π β β*)) β (β‘πΉ β (π€(ballβπ)π)) β π½) |
30 | 29 | ralrimivva 3199 |
. . . 4
β’ (π β βπ€ β π βπ β β* (β‘πΉ β (π€(ballβπ)π)) β π½) |
31 | | fveq2 6891 |
. . . . . . . 8
β’ (π§ = β¨π€, πβ© β ((ballβπ)βπ§) = ((ballβπ)ββ¨π€, πβ©)) |
32 | | df-ov 7415 |
. . . . . . . 8
β’ (π€(ballβπ)π) = ((ballβπ)ββ¨π€, πβ©) |
33 | 31, 32 | eqtr4di 2789 |
. . . . . . 7
β’ (π§ = β¨π€, πβ© β ((ballβπ)βπ§) = (π€(ballβπ)π)) |
34 | 33 | imaeq2d 6059 |
. . . . . 6
β’ (π§ = β¨π€, πβ© β (β‘πΉ β ((ballβπ)βπ§)) = (β‘πΉ β (π€(ballβπ)π))) |
35 | 34 | eleq1d 2817 |
. . . . 5
β’ (π§ = β¨π€, πβ© β ((β‘πΉ β ((ballβπ)βπ§)) β π½ β (β‘πΉ β (π€(ballβπ)π)) β π½)) |
36 | 35 | ralxp 5841 |
. . . 4
β’
(βπ§ β
(π Γ
β*)(β‘πΉ β ((ballβπ)βπ§)) β π½ β βπ€ β π βπ β β* (β‘πΉ β (π€(ballβπ)π)) β π½) |
37 | 30, 36 | sylibr 233 |
. . 3
β’ (π β βπ§ β (π Γ β*)(β‘πΉ β ((ballβπ)βπ§)) β π½) |
38 | | blf 24134 |
. . . 4
β’ (π β (βMetβπ) β (ballβπ):(π Γ
β*)βΆπ« π) |
39 | | ffn 6717 |
. . . 4
β’
((ballβπ):(π Γ
β*)βΆπ« π β (ballβπ) Fn (π Γ
β*)) |
40 | | imaeq2 6055 |
. . . . . 6
β’ (π’ = ((ballβπ)βπ§) β (β‘πΉ β π’) = (β‘πΉ β ((ballβπ)βπ§))) |
41 | 40 | eleq1d 2817 |
. . . . 5
β’ (π’ = ((ballβπ)βπ§) β ((β‘πΉ β π’) β π½ β (β‘πΉ β ((ballβπ)βπ§)) β π½)) |
42 | 41 | ralrn 7089 |
. . . 4
β’
((ballβπ) Fn
(π Γ
β*) β (βπ’ β ran (ballβπ)(β‘πΉ β π’) β π½ β βπ§ β (π Γ β*)(β‘πΉ β ((ballβπ)βπ§)) β π½)) |
43 | 3, 38, 39, 42 | 4syl 19 |
. . 3
β’ (π β (βπ’ β ran (ballβπ)(β‘πΉ β π’) β π½ β βπ§ β (π Γ β*)(β‘πΉ β ((ballβπ)βπ§)) β π½)) |
44 | 37, 43 | mpbird 257 |
. 2
β’ (π β βπ’ β ran (ballβπ)(β‘πΉ β π’) β π½) |
45 | 26 | mopntopon 24166 |
. . . 4
β’ (π β (βMetβπ) β π½ β (TopOnβπ)) |
46 | 2, 45 | syl 17 |
. . 3
β’ (π β π½ β (TopOnβπ)) |
47 | | ismtyhmeo.2 |
. . . . 5
β’ πΎ = (MetOpenβπ) |
48 | 47 | mopnval 24165 |
. . . 4
β’ (π β (βMetβπ) β πΎ = (topGenβran (ballβπ))) |
49 | 3, 48 | syl 17 |
. . 3
β’ (π β πΎ = (topGenβran (ballβπ))) |
50 | 47 | mopntopon 24166 |
. . . 4
β’ (π β (βMetβπ) β πΎ β (TopOnβπ)) |
51 | 3, 50 | syl 17 |
. . 3
β’ (π β πΎ β (TopOnβπ)) |
52 | 46, 49, 51 | tgcn 22977 |
. 2
β’ (π β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ’ β ran (ballβπ)(β‘πΉ β π’) β π½))) |
53 | 9, 44, 52 | mpbir2and 710 |
1
β’ (π β πΉ β (π½ Cn πΎ)) |