Step | Hyp | Ref
| Expression |
1 | | df-3an 1090 |
. . . . . . . 8
β’ ((π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β ((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
2 | | caucfil.1 |
. . . . . . . . . . . . . 14
β’ π =
(β€β₯βπ) |
3 | 2 | uztrn2 12789 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
4 | 3 | adantll 713 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
5 | | simpll3 1215 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β πΉ:πβΆπ) |
6 | 5 | fdmd 6684 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β dom πΉ = π) |
7 | 4, 6 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β π β dom πΉ) |
8 | 5, 4 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β π) |
9 | 7, 8 | jca 513 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β (π β dom πΉ β§ (πΉβπ) β π)) |
10 | 9 | biantrurd 534 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β (βπ β
(β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β ((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯))) |
11 | | uzss 12793 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β
(β€β₯βπ)) |
12 | 11 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β
(β€β₯βπ) β (β€β₯βπ)) |
13 | 12 | sseld 3948 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β (π β (β€β₯βπ) β π β (β€β₯βπ))) |
14 | 13 | pm4.71rd 564 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β (π β (β€β₯βπ) β (π β (β€β₯βπ) β§ π β (β€β₯βπ)))) |
15 | 14 | imbi1d 342 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β ((π β (β€β₯βπ) β§ π β (β€β₯βπ)) β ((πΉβπ)π·(πΉβπ)) < π₯))) |
16 | | impexp 452 |
. . . . . . . . . . 11
β’ (((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β ((πΉβπ)π·(πΉβπ)) < π₯) β (π β (β€β₯βπ) β (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯))) |
17 | 15, 16 | bitrdi 287 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β (π β (β€β₯βπ) β (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)))) |
18 | 17 | ralbidv2 3171 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β (βπ β
(β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯))) |
19 | 10, 18 | bitr3d 281 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β (((π β dom πΉ β§ (πΉβπ) β π) β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯))) |
20 | 1, 19 | bitrid 283 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ π β (β€β₯βπ)) β ((π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯))) |
21 | 20 | ralbidva 3173 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯))) |
22 | | r19.26-2 3136 |
. . . . . . . 8
β’
(βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β§ (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β§ βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯))) |
23 | | eleq1w 2821 |
. . . . . . . . . . . . 13
β’ (π’ = π β (π’ β (β€β₯βπ) β π β (β€β₯βπ))) |
24 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π’ = π β (πΉβπ’) = (πΉβπ)) |
25 | 24 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π’ = π β ((πΉβπ)π·(πΉβπ’)) = ((πΉβπ)π·(πΉβπ))) |
26 | 25 | breq1d 5120 |
. . . . . . . . . . . . 13
β’ (π’ = π β (((πΉβπ)π·(πΉβπ’)) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯)) |
27 | 23, 26 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π’ = π β ((π’ β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ’)) < π₯) β (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯))) |
28 | 27 | cbvralvw 3228 |
. . . . . . . . . . 11
β’
(βπ’ β
(β€β₯βπ)(π’ β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ’)) < π₯) β βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
29 | 28 | ralbii 3097 |
. . . . . . . . . 10
β’
(βπ β
(β€β₯βπ)βπ’ β (β€β₯βπ)(π’ β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ’)) < π₯) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
30 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
31 | 30 | eleq2d 2824 |
. . . . . . . . . . . 12
β’ (π = π β (π’ β (β€β₯βπ) β π’ β (β€β₯βπ))) |
32 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΉβπ) = (πΉβπ)) |
33 | 32 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉβπ)π·(πΉβπ’)) = ((πΉβπ)π·(πΉβπ’))) |
34 | 33 | breq1d 5120 |
. . . . . . . . . . . 12
β’ (π = π β (((πΉβπ)π·(πΉβπ’)) < π₯ β ((πΉβπ)π·(πΉβπ’)) < π₯)) |
35 | 31, 34 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = π β ((π’ β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ’)) < π₯) β (π’ β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ’)) < π₯))) |
36 | | eleq1w 2821 |
. . . . . . . . . . . 12
β’ (π’ = π β (π’ β (β€β₯βπ) β π β (β€β₯βπ))) |
37 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π’ = π β (πΉβπ’) = (πΉβπ)) |
38 | 37 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π’ = π β ((πΉβπ)π·(πΉβπ’)) = ((πΉβπ)π·(πΉβπ))) |
39 | 38 | breq1d 5120 |
. . . . . . . . . . . 12
β’ (π’ = π β (((πΉβπ)π·(πΉβπ’)) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯)) |
40 | 36, 39 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π’ = π β ((π’ β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ’)) < π₯) β (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯))) |
41 | 35, 40 | cbvral2vw 3230 |
. . . . . . . . . 10
β’
(βπ β
(β€β₯βπ)βπ’ β (β€β₯βπ)(π’ β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ’)) < π₯) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
42 | | ralcom 3275 |
. . . . . . . . . 10
β’
(βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
43 | 29, 41, 42 | 3bitr3i 301 |
. . . . . . . . 9
β’
(βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
44 | 43 | anbi2i 624 |
. . . . . . . 8
β’
((βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β§ βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β§ βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯))) |
45 | | anidm 566 |
. . . . . . . 8
β’
((βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β§ βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
46 | 22, 44, 45 | 3bitr2i 299 |
. . . . . . 7
β’
(βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β§ (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
47 | | simpll1 1213 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β π· β (βMetβπ)) |
48 | | simpll3 1215 |
. . . . . . . . . . . . . 14
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β πΉ:πβΆπ) |
49 | 2 | uztrn2 12789 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
50 | 49 | ad2ant2l 745 |
. . . . . . . . . . . . . 14
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β π β π) |
51 | 48, 50 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β (πΉβπ) β π) |
52 | 8 | adantrr 716 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β (πΉβπ) β π) |
53 | | xmetsym 23716 |
. . . . . . . . . . . . 13
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ (πΉβπ) β π) β ((πΉβπ)π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
54 | 47, 51, 52, 53 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β ((πΉβπ)π·(πΉβπ)) = ((πΉβπ)π·(πΉβπ))) |
55 | 54 | breq1d 5120 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β (((πΉβπ)π·(πΉβπ)) < π₯ β ((πΉβπ)π·(πΉβπ)) < π₯)) |
56 | 55 | imbi2d 341 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β ((π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯))) |
57 | 56 | anbi2d 630 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β (((π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β§ (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) β ((π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β§ (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)))) |
58 | | jaob 961 |
. . . . . . . . . 10
β’ (((π β
(β€β₯βπ) β¨ π β (β€β₯βπ)) β ((πΉβπ)π·(πΉβπ)) < π₯) β ((π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β§ (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯))) |
59 | | eluzelz 12780 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯βπ) β π β β€) |
60 | | eluzelz 12780 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯βπ) β π β β€) |
61 | | uztric 12794 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β€) β (π β
(β€β₯βπ) β¨ π β (β€β₯βπ))) |
62 | 59, 60, 61 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β (π β (β€β₯βπ) β¨ π β (β€β₯βπ))) |
63 | 62 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β (π β (β€β₯βπ) β¨ π β (β€β₯βπ))) |
64 | | pm5.5 362 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯βπ) β¨ π β (β€β₯βπ)) β (((π β (β€β₯βπ) β¨ π β (β€β₯βπ)) β ((πΉβπ)π·(πΉβπ)) < π₯) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β (((π β (β€β₯βπ) β¨ π β (β€β₯βπ)) β ((πΉβπ)π·(πΉβπ)) < π₯) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
66 | 58, 65 | bitr3id 285 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β (((π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β§ (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
67 | 57, 66 | bitrd 279 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β§ (π β (β€β₯βπ) β§ π β (β€β₯βπ))) β (((π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β§ (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) β ((πΉβπ)π·(πΉβπ)) < π₯)) |
68 | 67 | 2ralbidva 3211 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)((π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β§ (π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯)) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
69 | 46, 68 | bitr3id 285 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β (β€β₯βπ) β ((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
70 | 21, 69 | bitrd 279 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β§ π β π) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
71 | 70 | rexbidva 3174 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β (βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
72 | | uzf 12773 |
. . . . . 6
β’
β€β₯:β€βΆπ« β€ |
73 | | ffn 6673 |
. . . . . 6
β’
(β€β₯:β€βΆπ« β€ β
β€β₯ Fn β€) |
74 | 72, 73 | ax-mp 5 |
. . . . 5
β’
β€β₯ Fn β€ |
75 | | uzssz 12791 |
. . . . . 6
β’
(β€β₯βπ) β β€ |
76 | 2, 75 | eqsstri 3983 |
. . . . 5
β’ π β
β€ |
77 | | raleq 3312 |
. . . . . . 7
β’ (π’ =
(β€β₯βπ) β (βπ β π’ ((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
78 | 77 | raleqbi1dv 3310 |
. . . . . 6
β’ (π’ =
(β€β₯βπ) β (βπ β π’ βπ β π’ ((πΉβπ)π·(πΉβπ)) < π₯ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
79 | 78 | rexima 7192 |
. . . . 5
β’
((β€β₯ Fn β€ β§ π β β€) β (βπ’ β (β€β₯
β π)βπ β π’ βπ β π’ ((πΉβπ)π·(πΉβπ)) < π₯ β βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)) |
80 | 74, 76, 79 | mp2an 691 |
. . . 4
β’
(βπ’ β
(β€β₯ β π)βπ β π’ βπ β π’ ((πΉβπ)π·(πΉβπ)) < π₯ β βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) |
81 | 71, 80 | bitr4di 289 |
. . 3
β’ ((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β (βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ’ β (β€β₯ β π)βπ β π’ βπ β π’ ((πΉβπ)π·(πΉβπ)) < π₯)) |
82 | 81 | ralbidv 3175 |
. 2
β’ ((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯) β βπ₯ β β+ βπ’ β (β€β₯
β π)βπ β π’ βπ β π’ ((πΉβπ)π·(πΉβπ)) < π₯)) |
83 | | elfvdm 6884 |
. . . . . . 7
β’ (π· β (βMetβπ) β π β dom βMet) |
84 | 83 | adantr 482 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β β€) β π β dom βMet) |
85 | | cnex 11139 |
. . . . . 6
β’ β
β V |
86 | 84, 85 | jctir 522 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β β€) β (π β dom βMet β§ β β
V)) |
87 | | zsscn 12514 |
. . . . . . 7
β’ β€
β β |
88 | 76, 87 | sstri 3958 |
. . . . . 6
β’ π β
β |
89 | 88 | jctr 526 |
. . . . 5
β’ (πΉ:πβΆπ β (πΉ:πβΆπ β§ π β β)) |
90 | | elpm2r 8790 |
. . . . 5
β’ (((π β dom βMet β§
β β V) β§ (πΉ:πβΆπ β§ π β β)) β πΉ β (π βpm
β)) |
91 | 86, 89, 90 | syl2an 597 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β β€) β§ πΉ:πβΆπ) β πΉ β (π βpm
β)) |
92 | | simpl 484 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β β€) β π· β (βMetβπ)) |
93 | | simpr 486 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β β€) β π β β€) |
94 | 2, 92, 93 | iscau3 24658 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β β€) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)))) |
95 | 94 | baibd 541 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β β€) β§ πΉ β (π βpm β)) β (πΉ β (Cauβπ·) β βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯))) |
96 | 91, 95 | syldan 592 |
. . 3
β’ (((π· β (βMetβπ) β§ π β β€) β§ πΉ:πβΆπ) β (πΉ β (Cauβπ·) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯))) |
97 | 96 | 3impa 1111 |
. 2
β’ ((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β (πΉ β (Cauβπ·) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯))) |
98 | | caucfil.2 |
. . . 4
β’ πΏ = ((π FilMap πΉ)β(β€β₯ β
π)) |
99 | 98 | eleq1i 2829 |
. . 3
β’ (πΏ β (CauFilβπ·) β ((π FilMap πΉ)β(β€β₯ β
π)) β
(CauFilβπ·)) |
100 | 2 | uzfbas 23265 |
. . . 4
β’ (π β β€ β
(β€β₯ β π) β (fBasβπ)) |
101 | | fmcfil 24652 |
. . . 4
β’ ((π· β (βMetβπ) β§ (β€β₯
β π) β
(fBasβπ) β§ πΉ:πβΆπ) β (((π FilMap πΉ)β(β€β₯ β
π)) β
(CauFilβπ·) β
βπ₯ β
β+ βπ’ β (β€β₯ β π)βπ β π’ βπ β π’ ((πΉβπ)π·(πΉβπ)) < π₯)) |
102 | 100, 101 | syl3an2 1165 |
. . 3
β’ ((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β (((π FilMap πΉ)β(β€β₯ β
π)) β
(CauFilβπ·) β
βπ₯ β
β+ βπ’ β (β€β₯ β π)βπ β π’ βπ β π’ ((πΉβπ)π·(πΉβπ)) < π₯)) |
103 | 99, 102 | bitrid 283 |
. 2
β’ ((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β (πΏ β (CauFilβπ·) β βπ₯ β β+ βπ’ β (β€β₯
β π)βπ β π’ βπ β π’ ((πΉβπ)π·(πΉβπ)) < π₯)) |
104 | 82, 97, 103 | 3bitr4d 311 |
1
β’ ((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β (πΉ β (Cauβπ·) β πΏ β (CauFilβπ·))) |