Step | Hyp | Ref
| Expression |
1 | | lmle.1 |
. . . 4
β’ π =
(β€β₯βπ) |
2 | | lmle.4 |
. . . . 5
β’ (π β π· β (βMetβπ)) |
3 | | lmle.3 |
. . . . . 6
β’ π½ = (MetOpenβπ·) |
4 | 3 | mopntopon 23815 |
. . . . 5
β’ (π· β (βMetβπ) β π½ β (TopOnβπ)) |
5 | 2, 4 | syl 17 |
. . . 4
β’ (π β π½ β (TopOnβπ)) |
6 | | lmle.6 |
. . . 4
β’ (π β π β β€) |
7 | | lmrel 22604 |
. . . . 5
β’ Rel
(βπ‘βπ½) |
8 | | lmle.7 |
. . . . 5
β’ (π β πΉ(βπ‘βπ½)π) |
9 | | releldm 5903 |
. . . . 5
β’ ((Rel
(βπ‘βπ½) β§ πΉ(βπ‘βπ½)π) β πΉ β dom
(βπ‘βπ½)) |
10 | 7, 8, 9 | sylancr 588 |
. . . 4
β’ (π β πΉ β dom
(βπ‘βπ½)) |
11 | 1, 5, 6, 10 | lmff 22675 |
. . 3
β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ) |
12 | | eqid 2733 |
. . . 4
β’
(β€β₯βπ) = (β€β₯βπ) |
13 | 5 | adantr 482 |
. . . 4
β’ ((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β π½ β (TopOnβπ)) |
14 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β π β π) |
15 | 14, 1 | eleqtrdi 2844 |
. . . . 5
β’ ((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β π β (β€β₯βπ)) |
16 | | eluzelz 12781 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β β€) |
17 | 15, 16 | syl 17 |
. . . 4
β’ ((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β π β β€) |
18 | 8 | adantr 482 |
. . . 4
β’ ((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β πΉ(βπ‘βπ½)π) |
19 | | oveq2 7369 |
. . . . . 6
β’ (π₯ = (πΉβπ) β (ππ·π₯) = (ππ·(πΉβπ))) |
20 | 19 | breq1d 5119 |
. . . . 5
β’ (π₯ = (πΉβπ) β ((ππ·π₯) β€ π
β (ππ·(πΉβπ)) β€ π
)) |
21 | | fvres 6865 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β ((πΉ βΎ (β€β₯βπ))βπ) = (πΉβπ)) |
22 | 21 | adantl 483 |
. . . . . 6
β’ (((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β§ π β (β€β₯βπ)) β ((πΉ βΎ (β€β₯βπ))βπ) = (πΉβπ)) |
23 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ) |
24 | 23 | ffvelcdmda 7039 |
. . . . . 6
β’ (((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β§ π β (β€β₯βπ)) β ((πΉ βΎ (β€β₯βπ))βπ) β π) |
25 | 22, 24 | eqeltrrd 2835 |
. . . . 5
β’ (((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β§ π β (β€β₯βπ)) β (πΉβπ) β π) |
26 | 1 | uztrn2 12790 |
. . . . . . 7
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
27 | 14, 26 | sylan 581 |
. . . . . 6
β’ (((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β§ π β (β€β₯βπ)) β π β π) |
28 | | lmle.10 |
. . . . . . 7
β’ ((π β§ π β π) β (ππ·(πΉβπ)) β€ π
) |
29 | 28 | adantlr 714 |
. . . . . 6
β’ (((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β§ π β π) β (ππ·(πΉβπ)) β€ π
) |
30 | 27, 29 | syldan 592 |
. . . . 5
β’ (((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β§ π β (β€β₯βπ)) β (ππ·(πΉβπ)) β€ π
) |
31 | 20, 25, 30 | elrabd 3651 |
. . . 4
β’ (((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β§ π β (β€β₯βπ)) β (πΉβπ) β {π₯ β π β£ (ππ·π₯) β€ π
}) |
32 | | lmle.8 |
. . . . . 6
β’ (π β π β π) |
33 | | lmle.9 |
. . . . . 6
β’ (π β π
β
β*) |
34 | | eqid 2733 |
. . . . . . 7
β’ {π₯ β π β£ (ππ·π₯) β€ π
} = {π₯ β π β£ (ππ·π₯) β€ π
} |
35 | 3, 34 | blcld 23884 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β {π₯ β π β£ (ππ·π₯) β€ π
} β (Clsdβπ½)) |
36 | 2, 32, 33, 35 | syl3anc 1372 |
. . . . 5
β’ (π β {π₯ β π β£ (ππ·π₯) β€ π
} β (Clsdβπ½)) |
37 | 36 | adantr 482 |
. . . 4
β’ ((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β {π₯ β π β£ (ππ·π₯) β€ π
} β (Clsdβπ½)) |
38 | 12, 13, 17, 18, 31, 37 | lmcld 22677 |
. . 3
β’ ((π β§ (π β π β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ)) β π β {π₯ β π β£ (ππ·π₯) β€ π
}) |
39 | 11, 38 | rexlimddv 3155 |
. 2
β’ (π β π β {π₯ β π β£ (ππ·π₯) β€ π
}) |
40 | | oveq2 7369 |
. . . . 5
β’ (π₯ = π β (ππ·π₯) = (ππ·π)) |
41 | 40 | breq1d 5119 |
. . . 4
β’ (π₯ = π β ((ππ·π₯) β€ π
β (ππ·π) β€ π
)) |
42 | 41 | elrab 3649 |
. . 3
β’ (π β {π₯ β π β£ (ππ·π₯) β€ π
} β (π β π β§ (ππ·π) β€ π
)) |
43 | 42 | simprbi 498 |
. 2
β’ (π β {π₯ β π β£ (ππ·π₯) β€ π
} β (ππ·π) β€ π
) |
44 | 39, 43 | syl 17 |
1
β’ (π β (ππ·π) β€ π
) |