Step | Hyp | Ref
| Expression |
1 | | n0 4305 |
. . 3
β’ (π β β
β
βπ§ π§ β π) |
2 | | metxmet 23609 |
. . . . . . . . 9
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
3 | | metdscn.f |
. . . . . . . . . 10
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
4 | 3 | metdsf 24133 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π β π) β πΉ:πβΆ(0[,]+β)) |
5 | 2, 4 | sylan 581 |
. . . . . . . 8
β’ ((π· β (Metβπ) β§ π β π) β πΉ:πβΆ(0[,]+β)) |
6 | 5 | adantr 482 |
. . . . . . 7
β’ (((π· β (Metβπ) β§ π β π) β§ π§ β π) β πΉ:πβΆ(0[,]+β)) |
7 | 6 | ffnd 6665 |
. . . . . 6
β’ (((π· β (Metβπ) β§ π β π) β§ π§ β π) β πΉ Fn π) |
8 | 5 | adantr 482 |
. . . . . . . . . . 11
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β πΉ:πβΆ(0[,]+β)) |
9 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β π€ β π) |
10 | 8, 9 | ffvelcdmd 7031 |
. . . . . . . . . 10
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) β (0[,]+β)) |
11 | | eliccxr 13281 |
. . . . . . . . . 10
β’ ((πΉβπ€) β (0[,]+β) β (πΉβπ€) β
β*) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) β
β*) |
13 | | simpll 766 |
. . . . . . . . . 10
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β π· β (Metβπ)) |
14 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π· β (Metβπ) β§ π β π) β π β π) |
15 | 14 | sselda 3943 |
. . . . . . . . . . 11
β’ (((π· β (Metβπ) β§ π β π) β§ π§ β π) β π§ β π) |
16 | 15 | adantrr 716 |
. . . . . . . . . 10
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β π§ β π) |
17 | | metcl 23607 |
. . . . . . . . . 10
β’ ((π· β (Metβπ) β§ π§ β π β§ π€ β π) β (π§π·π€) β β) |
18 | 13, 16, 9, 17 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β (π§π·π€) β β) |
19 | | elxrge0 13303 |
. . . . . . . . . . 11
β’ ((πΉβπ€) β (0[,]+β) β ((πΉβπ€) β β* β§ 0 β€
(πΉβπ€))) |
20 | 19 | simprbi 498 |
. . . . . . . . . 10
β’ ((πΉβπ€) β (0[,]+β) β 0 β€ (πΉβπ€)) |
21 | 10, 20 | syl 17 |
. . . . . . . . 9
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β 0 β€ (πΉβπ€)) |
22 | 3 | metdsle 24137 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) β€ (π§π·π€)) |
23 | 2, 22 | sylanl1 679 |
. . . . . . . . 9
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) β€ (π§π·π€)) |
24 | | xrrege0 13022 |
. . . . . . . . 9
β’ ((((πΉβπ€) β β* β§ (π§π·π€) β β) β§ (0 β€ (πΉβπ€) β§ (πΉβπ€) β€ (π§π·π€))) β (πΉβπ€) β β) |
25 | 12, 18, 21, 23, 24 | syl22anc 838 |
. . . . . . . 8
β’ (((π· β (Metβπ) β§ π β π) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) β β) |
26 | 25 | anassrs 469 |
. . . . . . 7
β’ ((((π· β (Metβπ) β§ π β π) β§ π§ β π) β§ π€ β π) β (πΉβπ€) β β) |
27 | 26 | ralrimiva 3142 |
. . . . . 6
β’ (((π· β (Metβπ) β§ π β π) β§ π§ β π) β βπ€ β π (πΉβπ€) β β) |
28 | | ffnfv 7061 |
. . . . . 6
β’ (πΉ:πβΆβ β (πΉ Fn π β§ βπ€ β π (πΉβπ€) β β)) |
29 | 7, 27, 28 | sylanbrc 584 |
. . . . 5
β’ (((π· β (Metβπ) β§ π β π) β§ π§ β π) β πΉ:πβΆβ) |
30 | 29 | ex 414 |
. . . 4
β’ ((π· β (Metβπ) β§ π β π) β (π§ β π β πΉ:πβΆβ)) |
31 | 30 | exlimdv 1937 |
. . 3
β’ ((π· β (Metβπ) β§ π β π) β (βπ§ π§ β π β πΉ:πβΆβ)) |
32 | 1, 31 | biimtrid 241 |
. 2
β’ ((π· β (Metβπ) β§ π β π) β (π β β
β πΉ:πβΆβ)) |
33 | 32 | 3impia 1118 |
1
β’ ((π· β (Metβπ) β§ π β π β§ π β β
) β πΉ:πβΆβ) |