Step | Hyp | Ref
| Expression |
1 | | n0 4304 |
. . 3
β’ (π β β
β
βπ§ π§ β π) |
2 | | metxmet 23609 |
. . . . . . . . 9
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
3 | | metdscn.f |
. . . . . . . . . 10
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
4 | 3 | metdsf 24133 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π β π) β πΉ:πβΆ(0[,]+β)) |
5 | 2, 4 | sylan 580 |
. . . . . . . 8
β’ ((π· β (Metβπ) β§ π β π) β πΉ:πβΆ(0[,]+β)) |
6 | 5 | adantr 481 |
. . . . . . 7
β’ (((π· β (Metβπ) β§ π β π) β§ π§ β π) β πΉ:πβΆ(0[,]+β)) |
7 | 6 | ffnd 6664 |
. . . . . 6
β’ (((π· β (Metβπ) β§ π β π) β§ π§ β π) β πΉ Fn π) |
8 | 5 | adantr 481 |
. . . . . . . . . . 11
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β πΉ:πβΆ(0[,]+β)) |
9 | | simprr 771 |
. . . . . . . . . . 11
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β π€ β π) |
10 | 8, 9 | ffvelcdmd 7030 |
. . . . . . . . . 10
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) β (0[,]+β)) |
11 | | eliccxr 13280 |
. . . . . . . . . 10
β’ ((πΉβπ€) β (0[,]+β) β (πΉβπ€) β
β*) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) β
β*) |
13 | | simpll 765 |
. . . . . . . . . 10
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β π· β (Metβπ)) |
14 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((π· β (Metβπ) β§ π β π) β π β π) |
15 | 14 | sselda 3942 |
. . . . . . . . . . 11
β’ (((π· β (Metβπ) β§ π β π) β§ π§ β π) β π§ β π) |
16 | 15 | adantrr 715 |
. . . . . . . . . 10
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β π§ β π) |
17 | | metcl 23607 |
. . . . . . . . . 10
β’ ((π· β (Metβπ) β§ π§ β π β§ π€ β π) β (π§π·π€) β β) |
18 | 13, 16, 9, 17 | syl3anc 1371 |
. . . . . . . . 9
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β (π§π·π€) β β) |
19 | | elxrge0 13302 |
. . . . . . . . . . 11
β’ ((πΉβπ€) β (0[,]+β) β ((πΉβπ€) β β* β§ 0 β€
(πΉβπ€))) |
20 | 19 | simprbi 497 |
. . . . . . . . . 10
β’ ((πΉβπ€) β (0[,]+β) β 0 β€ (πΉβπ€)) |
21 | 10, 20 | syl 17 |
. . . . . . . . 9
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β 0 β€ (πΉβπ€)) |
22 | 3 | metdsle 24137 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) β€ (π§π·π€)) |
23 | 2, 22 | sylanl1 678 |
. . . . . . . . 9
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) β€ (π§π·π€)) |
24 | | xrrege0 13021 |
. . . . . . . . 9
β’ ((((πΉβπ€) β β* β§ (π§π·π€) β β) β§ (0 β€ (πΉβπ€) β§ (πΉβπ€) β€ (π§π·π€))) β (πΉβπ€) β β) |
25 | 12, 18, 21, 23, 24 | syl22anc 837 |
. . . . . . . 8
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) β β) |
26 | 25 | anassrs 468 |
. . . . . . 7
β’ ((((π· β (Metβπ) β§ π β π) β§ π§ β π) β§ π€ β π) β (πΉβπ€) β β) |
27 | 26 | ralrimiva 3141 |
. . . . . 6
β’ (((π· β (Metβπ) β§ π β π) β§ π§ β π) β βπ€ β π (πΉβπ€) β β) |
28 | | ffnfv 7060 |
. . . . . 6
β’ (πΉ:πβΆβ β (πΉ Fn π β§ βπ€ β π (πΉβπ€) β β)) |
29 | 7, 27, 28 | sylanbrc 583 |
. . . . 5
β’ (((π· β (Metβπ) β§ π β π) β§ π§ β π) β πΉ:πβΆβ) |
30 | 29 | ex 413 |
. . . 4
β’ ((π· β (Metβπ) β§ π β π) β (π§ β π β πΉ:πβΆβ)) |
31 | 30 | exlimdv 1936 |
. . 3
β’ ((π· β (Metβπ) β§ π β π) β (βπ§ π§ β π β πΉ:πβΆβ)) |
32 | 1, 31 | biimtrid 241 |
. 2
β’ ((π· β (Metβπ) β§ π β π) β (π β β
β πΉ:πβΆβ)) |
33 | 32 | 3impia 1117 |
1
β’ ((π· β (Metβπ) β§ π β π β§ π β β
) β πΉ:πβΆβ) |